Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjxiun Unicode version

Theorem disjxiun 4150
 Description: An indexed union of a disjoint collection of disjoint collections is disjoint if each component is disjoint, and the disjoint unions in the collection are also disjoint. Note that and may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016.)
Assertion
Ref Expression
disjxiun Disj Disj Disj Disj
Distinct variable groups:   ,,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem disjxiun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfiu1 4063 . . . . . 6
2 nfcv 2523 . . . . . 6
31, 2nfdisj 4135 . . . . 5 Disj
4 ssiun2 4075 . . . . . . 7
5 disjss1 4129 . . . . . . 7 Disj Disj
64, 5syl 16 . . . . . 6 Disj Disj
76com12 29 . . . . 5 Disj Disj
83, 7ralrimi 2730 . . . 4 Disj Disj
98a1i 11 . . 3 Disj Disj Disj
10 simplr 732 . . . . . . . . . 10 Disj Disj Disj
11 simprll 739 . . . . . . . . . . 11 Disj Disj
12 ssiun2 4075 . . . . . . . . . . . 12
13 nfcv 2523 . . . . . . . . . . . . 13
14 nfcsb1v 3226 . . . . . . . . . . . . 13
15 csbeq1a 3202 . . . . . . . . . . . . 13
1613, 14, 15cbviun 4069 . . . . . . . . . . . 12
1712, 16syl6sseqr 3338 . . . . . . . . . . 11
1811, 17syl 16 . . . . . . . . . 10 Disj Disj
19 simprlr 740 . . . . . . . . . . 11 Disj Disj
20 csbeq1 3197 . . . . . . . . . . . . 13
2120sseq1d 3318 . . . . . . . . . . . 12
2221, 17vtoclga 2960 . . . . . . . . . . 11
2319, 22syl 16 . . . . . . . . . 10 Disj Disj
24 simpl 444 . . . . . . . . . . . . . . . 16 Disj Disj Disj
2513, 14, 15cbvdisj 4133 . . . . . . . . . . . . . . . 16 Disj Disj
2624, 25sylib 189 . . . . . . . . . . . . . . 15 Disj Disj Disj
2720disjor 4137 . . . . . . . . . . . . . . 15 Disj
2826, 27sylib 189 . . . . . . . . . . . . . 14 Disj Disj
29 rsp2 2711 . . . . . . . . . . . . . 14
3028, 29syl 16 . . . . . . . . . . . . 13 Disj Disj
3130imp 419 . . . . . . . . . . . 12 Disj Disj
3231ord 367 . . . . . . . . . . 11 Disj Disj
3332impr 603 . . . . . . . . . 10 Disj Disj
34 disjiun 4143 . . . . . . . . . 10 Disj
3510, 18, 23, 33, 34syl13anc 1186 . . . . . . . . 9 Disj Disj
3635expr 599 . . . . . . . 8 Disj Disj
3736orrd 368 . . . . . . 7 Disj Disj
3837ralrimivva 2741 . . . . . 6 Disj Disj
3920iuneq1d 4058 . . . . . . 7
4039disjor 4137 . . . . . 6 Disj
4138, 40sylibr 204 . . . . 5 Disj Disj Disj
42 nfcv 2523 . . . . . 6
4314, 2nfiun 4061 . . . . . 6
4415iuneq1d 4058 . . . . . 6
4542, 43, 44cbvdisj 4133 . . . . 5 Disj Disj
4641, 45sylibr 204 . . . 4 Disj Disj Disj
4746ex 424 . . 3 Disj Disj Disj
489, 47jcad 520 . 2 Disj Disj Disj Disj
4916eleq2i 2451 . . . . . . . . 9
50 eliun 4039 . . . . . . . . 9
5149, 50bitri 241 . . . . . . . 8
52 nfcv 2523 . . . . . . . . . . 11
53 nfcsb1v 3226 . . . . . . . . . . 11
54 csbeq1a 3202 . . . . . . . . . . 11
5552, 53, 54cbviun 4069 . . . . . . . . . 10
5655eleq2i 2451 . . . . . . . . 9
57 eliun 4039 . . . . . . . . 9
5856, 57bitri 241 . . . . . . . 8
5951, 58anbi12i 679 . . . . . . 7
60 reeanv 2818 . . . . . . 7
6159, 60bitr4i 244 . . . . . 6
62 simplrr 738 . . . . . . . . . . . 12 Disj Disj Disj
63 simprl 733 . . . . . . . . . . . . . . . . 17 Disj Disj Disj
64 simplrl 737 . . . . . . . . . . . . . . . . 17 Disj Disj Disj Disj
6514, 2nfdisj 4135 . . . . . . . . . . . . . . . . . 18 Disj
6615disjeq1d 4131 . . . . . . . . . . . . . . . . . 18 Disj Disj
6765, 66rspc 2989 . . . . . . . . . . . . . . . . 17 Disj Disj
6863, 64, 67sylc 58 . . . . . . . . . . . . . . . 16 Disj Disj Disj Disj
6968ad2antrr 707 . . . . . . . . . . . . . . 15 Disj Disj Disj Disj
70 disjors 4139 . . . . . . . . . . . . . . 15 Disj
7169, 70sylib 189 . . . . . . . . . . . . . 14 Disj Disj Disj
72 simplrl 737 . . . . . . . . . . . . . . . 16 Disj Disj Disj
7372simpld 446 . . . . . . . . . . . . . . 15 Disj Disj Disj
7472simprd 450 . . . . . . . . . . . . . . . 16 Disj Disj Disj
7520adantl 453 . . . . . . . . . . . . . . . 16 Disj Disj Disj
7674, 75eleqtrrd 2464 . . . . . . . . . . . . . . 15 Disj Disj Disj
7773, 76jca 519 . . . . . . . . . . . . . 14 Disj Disj Disj
78 rsp2 2711 . . . . . . . . . . . . . 14
7971, 77, 78sylc 58 . . . . . . . . . . . . 13 Disj Disj Disj
8079ord 367 . . . . . . . . . . . 12 Disj Disj Disj
8162, 80mpd 15 . . . . . . . . . . 11 Disj Disj Disj
82 simplrl 737 . . . . . . . . . . . . . . 15 Disj Disj Disj
8382simpld 446 . . . . . . . . . . . . . 14 Disj Disj Disj
84 ssiun2 4075 . . . . . . . . . . . . . . 15
85 nfcv 2523 . . . . . . . . . . . . . . . 16
86 nfcsb1v 3226 . . . . . . . . . . . . . . . 16
87 csbeq1a 3202 . . . . . . . . . . . . . . . 16
8885, 86, 87cbviun 4069 . . . . . . . . . . . . . . 15
8984, 88syl6sseqr 3338 . . . . . . . . . . . . . 14
9083, 89syl 16 . . . . . . . . . . . . 13 Disj Disj Disj
9182simprd 450 . . . . . . . . . . . . . 14 Disj Disj Disj
92 ssiun2 4075 . . . . . . . . . . . . . . 15
93 nfcv 2523 . . . . . . . . . . . . . . . 16
94 nfcsb1v 3226 . . . . . . . . . . . . . . . 16
95 csbeq1a 3202 . . . . . . . . . . . . . . . 16
9693, 94, 95cbviun 4069 . . . . . . . . . . . . . . 15
9792, 96syl6sseqr 3338 . . . . . . . . . . . . . 14
9891, 97syl 16 . . . . . . . . . . . . 13 Disj Disj Disj
99 ss2in 3511 . . . . . . . . . . . . 13
10090, 98, 99syl2anc 643 . . . . . . . . . . . 12 Disj Disj Disj
101 simplrr 738 . . . . . . . . . . . . . . 15 Disj Disj Disj Disj
102101ad2antrr 707 . . . . . . . . . . . . . 14 Disj Disj Disj Disj
103 nfcv 2523 . . . . . . . . . . . . . . 15
104 nfcsb1v 3226 . . . . . . . . . . . . . . . 16
105104, 2nfiun 4061 . . . . . . . . . . . . . . 15
106 csbeq1a 3202 . . . . . . . . . . . . . . . 16
107106iuneq1d 4058 . . . . . . . . . . . . . . 15
108103, 105, 107cbvdisj 4133 . . . . . . . . . . . . . 14 Disj Disj
109102, 108sylib 189 . . . . . . . . . . . . 13 Disj Disj Disj Disj
11063ad2antrr 707 . . . . . . . . . . . . 13 Disj Disj Disj
111 simprr 734 . . . . . . . . . . . . . 14 Disj Disj Disj
112111ad2antrr 707 . . . . . . . . . . . . 13 Disj Disj Disj
113 simpr 448 . . . . . . . . . . . . 13 Disj Disj Disj
114 csbeq1 3197 . . . . . . . . . . . . . . 15
115114iuneq1d 4058 . . . . . . . . . . . . . 14
116 csbeq1 3197 . . . . . . . . . . . . . . 15
117116iuneq1d 4058 . . . . . . . . . . . . . 14
118115, 117disji2 4140 . . . . . . . . . . . . 13 Disj
119109, 110, 112, 113, 118syl121anc 1189 . . . . . . . . . . . 12 Disj Disj Disj
120 sseq0 3602 . . . . . . . . . . . 12
121100, 119, 120syl2anc 643 . . . . . . . . . . 11 Disj Disj Disj
12281, 121pm2.61dane 2628 . . . . . . . . . 10 Disj Disj Disj
123122expr 599 . . . . . . . . 9 Disj Disj Disj
124123orrd 368 . . . . . . . 8 Disj Disj Disj
125124ex 424 . . . . . . 7 Disj Disj Disj
126125rexlimdvva 2780 . . . . . 6 Disj Disj Disj
12761, 126syl5bi 209 . . . . 5 Disj Disj Disj
128127ralrimivv 2740 . . . 4 Disj Disj Disj
129 disjors 4139 . . . 4 Disj
130128, 129sylibr 204 . . 3 Disj Disj Disj Disj
131130ex 424 . 2 Disj Disj Disj Disj
13248, 131impbid 184 1 Disj Disj Disj Disj
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   wceq 1649   wcel 1717   wne 2550  wral 2649  wrex 2650  csb 3194   cin 3262   wss 3263  c0 3571  ciun 4035  Disj wdisj 4123 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-reu 2656  df-rmo 2657  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-in 3270  df-ss 3277  df-nul 3572  df-iun 4037  df-disj 4124
 Copyright terms: Public domain W3C validator