MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjxiun Structured version   Visualization version   Unicode version
Theorem disjxiun 4649
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 B ( y ) and C ( x ) may have the displayed free variables. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by JJ, 27-May-2021.)
Assertion
Ref Expression
disjxiun |- (Disj y e. A B -> (Disj x e. U_ y e. A B C <-> ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) ) )
Distinct variable groups:   x, y, A   x, B   y, C
Allowed substitution hints:   B( y)   C( x)
Proof of Theorem disjxiun
Dummy variables s r u v z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfiu1 4550 . . . . . 6 |- F/_ y U_ y e. A B
2 nfcv 2764 . . . . . 6 |- F/_ y C
31, 2nfdisj 4632 . . . . 5 |- F/ yDisj x e. U_ y e. A B C
4 disjss1 4626 . . . . . 6 |- ( B C_ U_ y e. A B -> (Disj x e. U_ y e. A B C -> Disj x e. B C ) )
5 ssiun2 4563 . . . . . 6 |- ( y e. A -> B C_ U_ y e. A B )
64, 5syl11 33 . . . . 5 |- (Disj x e. U_ y e. A B C -> ( y e. A -> Disj x e. B C ) )
73, 6ralrimi 2957 . . . 4 |- (Disj x e. U_ y e. A B C -> A. y e. A Disj x e. B C )
87a1i 11 . . 3 |- (Disj y e. A B -> (Disj x e. U_ y e. A B C -> A. y e. A Disj x e. B C ) )
9 simplr 792 . . . . . . . . . 10 |- ( ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) /\ ( ( u e. A /\ v e. A ) /\ -. u = v ) ) -> Disj x e. U_ y e. A B C )
10 ssiun2 4563 . . . . . . . . . . . . 13 |- ( u e. A -> [_ u / y ]_ B C_ U_ u e. A [_ u / y ]_ B )
11 nfcv 2764 . . . . . . . . . . . . . 14 |- F/_ u B
12 nfcsb1v 3549 . . . . . . . . . . . . . 14 |- F/_ y [_ u / y ]_ B
13 csbeq1a 3542 . . . . . . . . . . . . . 14 |- ( y = u -> B = [_ u / y ]_ B )
1411, 12, 13cbviun 4557 . . . . . . . . . . . . 13 |- U_ y e. A B = U_ u e. A [_ u / y ]_ B
1510, 14syl6sseqr 3652 . . . . . . . . . . . 12 |- ( u e. A -> [_ u / y ]_ B C_ U_ y e. A B )
1615adantr 481 . . . . . . . . . . 11 |- ( ( u e. A /\ v e. A ) -> [_ u / y ]_ B C_ U_ y e. A B )
1716ad2antrl 764 . . . . . . . . . 10 |- ( ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) /\ ( ( u e. A /\ v e. A ) /\ -. u = v ) ) -> [_ u / y ]_ B C_ U_ y e. A B )
18 csbeq1 3536 . . . . . . . . . . . . . 14 |- ( u = v -> [_ u / y ]_ B = [_ v / y ]_ B )
1918sseq1d 3632 . . . . . . . . . . . . 13 |- ( u = v -> ( [_ u / y ]_ B C_ U_ y e. A B <-> [_ v / y ]_ B C_ U_ y e. A B ) )
2019, 15vtoclga 3272 . . . . . . . . . . . 12 |- ( v e. A -> [_ v / y ]_ B C_ U_ y e. A B )
2120adantl 482 . . . . . . . . . . 11 |- ( ( u e. A /\ v e. A ) -> [_ v / y ]_ B C_ U_ y e. A B )
2221ad2antrl 764 . . . . . . . . . 10 |- ( ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) /\ ( ( u e. A /\ v e. A ) /\ -. u = v ) ) -> [_ v / y ]_ B C_ U_ y e. A B )
2311, 12, 13cbvdisj 4630 . . . . . . . . . . . . . . . 16 |- (Disj y e. A B <-> Disj u e. A [_ u / y ]_ B )
2418disjor 4634 . . . . . . . . . . . . . . . 16 |- (Disj u e. A [_ u / y ]_ B <-> A. u e. A A. v e. A ( u = v \/ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) )
2523, 24sylbb 209 . . . . . . . . . . . . . . 15 |- (Disj y e. A B -> A. u e. A A. v e. A ( u = v \/ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) )
26 rsp2 2936 . . . . . . . . . . . . . . 15 |- ( A. u e. A A. v e. A ( u = v \/ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) -> ( ( u e. A /\ v e. A ) -> ( u = v \/ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) ) )
2725, 26syl 17 . . . . . . . . . . . . . 14 |- (Disj y e. A B -> ( ( u e. A /\ v e. A ) -> ( u = v \/ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) ) )
2827imp 445 . . . . . . . . . . . . 13 |- ( (Disj y e. A B /\ ( u e. A /\ v e. A ) ) -> ( u = v \/ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) )
2928ord 392 . . . . . . . . . . . 12 |- ( (Disj y e. A B /\ ( u e. A /\ v e. A ) ) -> ( -. u = v -> ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) )
3029impr 649 . . . . . . . . . . 11 |- ( (Disj y e. A B /\ ( ( u e. A /\ v e. A ) /\ -. u = v ) ) -> ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) )
3130adantlr 751 . . . . . . . . . 10 |- ( ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) /\ ( ( u e. A /\ v e. A ) /\ -. u = v ) ) -> ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) )
32 disjiun 4640 . . . . . . . . . 10 |- ( (Disj x e. U_ y e. A B C /\ ( [_ u / y ]_ B C_ U_ y e. A B /\ [_ v / y ]_ B C_ U_ y e. A B /\ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) ) -> ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) )
339, 17, 22, 31, 32syl13anc 1328 . . . . . . . . 9 |- ( ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) /\ ( ( u e. A /\ v e. A ) /\ -. u = v ) ) -> ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) )
3433expr 643 . . . . . . . 8 |- ( ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) /\ ( u e. A /\ v e. A ) ) -> ( -. u = v -> ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) ) )
3534orrd 393 . . . . . . 7 |- ( ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) /\ ( u e. A /\ v e. A ) ) -> ( u = v \/ ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) ) )
3635ralrimivva 2971 . . . . . 6 |- ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) -> A. u e. A A. v e. A ( u = v \/ ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) ) )
3718iuneq1d 4545 . . . . . . 7 |- ( u = v -> U_ x e. [_ u / y ]_ B C = U_ x e. [_ v / y ]_ B C )
3837disjor 4634 . . . . . 6 |- (Disj u e. A U_ x e. [_ u / y ]_ B C <-> A. u e. A A. v e. A ( u = v \/ ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) ) )
3936, 38sylibr 224 . . . . 5 |- ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) -> Disj u e. A U_ x e. [_ u / y ]_ B C )
40 nfcv 2764 . . . . . 6 |- F/_ u U_ x e. B C
4112, 2nfiun 4548 . . . . . 6 |- F/_ y U_ x e. [_ u / y ]_ B C
4213iuneq1d 4545 . . . . . 6 |- ( y = u -> U_ x e. B C = U_ x e. [_ u / y ]_ B C )
4340, 41, 42cbvdisj 4630 . . . . 5 |- (Disj y e. A U_ x e. B C <-> Disj u e. A U_ x e. [_ u / y ]_ B C )
4439, 43sylibr 224 . . . 4 |- ( (Disj y e. A B /\ Disj x e. U_ y e. A B C ) -> Disj y e. A U_ x e. B C )
4544ex 450 . . 3 |- (Disj y e. A B -> (Disj x e. U_ y e. A B C -> Disj y e. A U_ x e. B C ) )
468, 45jcad 555 . 2 |- (Disj y e. A B -> (Disj x e. U_ y e. A B C -> ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) ) )
4714eleq2i 2693 . . . . . . . 8 |- ( r e. U_ y e. A B <-> r e. U_ u e. A [_ u / y ]_ B )
48 eliun 4524 . . . . . . . 8 |- ( r e. U_ u e. A [_ u / y ]_ B <-> E. u e. A r e. [_ u / y ]_ B )
4947, 48bitri 264 . . . . . . 7 |- ( r e. U_ y e. A B <-> E. u e. A r e. [_ u / y ]_ B )
50 nfcv 2764 . . . . . . . . . 10 |- F/_ v B
51 nfcsb1v 3549 . . . . . . . . . 10 |- F/_ y [_ v / y ]_ B
52 csbeq1a 3542 . . . . . . . . . 10 |- ( y = v -> B = [_ v / y ]_ B )
5350, 51, 52cbviun 4557 . . . . . . . . 9 |- U_ y e. A B = U_ v e. A [_ v / y ]_ B
5453eleq2i 2693 . . . . . . . 8 |- ( s e. U_ y e. A B <-> s e. U_ v e. A [_ v / y ]_ B )
55 eliun 4524 . . . . . . . 8 |- ( s e. U_ v e. A [_ v / y ]_ B <-> E. v e. A s e. [_ v / y ]_ B )
5654, 55bitri 264 . . . . . . 7 |- ( s e. U_ y e. A B <-> E. v e. A s e. [_ v / y ]_ B )
5749, 56anbi12i 733 . . . . . 6 |- ( ( r e. U_ y e. A B /\ s e. U_ y e. A B ) <-> ( E. u e. A r e. [_ u / y ]_ B /\ E. v e. A s e. [_ v / y ]_ B ) )
58 reeanv 3107 . . . . . 6 |- ( E. u e. A E. v e. A ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) <-> ( E. u e. A r e. [_ u / y ]_ B /\ E. v e. A s e. [_ v / y ]_ B ) )
5957, 58bitr4i 267 . . . . 5 |- ( ( r e. U_ y e. A B /\ s e. U_ y e. A B ) <-> E. u e. A E. v e. A ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) )
60 simplrr 801 . . . . . . . . . . 11 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) /\ u = v ) -> -. r = s )
6112, 2nfdisj 4632 . . . . . . . . . . . . . . . . . . 19 |- F/ yDisj x e. [_ u / y ]_ B C
6213disjeq1d 4628 . . . . . . . . . . . . . . . . . . 19 |- ( y = u -> (Disj x e. B C <-> Disj x e. [_ u / y ]_ B C ) )
6361, 62rspc 3303 . . . . . . . . . . . . . . . . . 18 |- ( u e. A -> ( A. y e. A Disj x e. B C -> Disj x e. [_ u / y ]_ B C ) )
6463impcom 446 . . . . . . . . . . . . . . . . 17 |- ( ( A. y e. A Disj x e. B C /\ u e. A ) -> Disj x e. [_ u / y ]_ B C )
65 disjors 4635 . . . . . . . . . . . . . . . . 17 |- (Disj x e. [_ u / y ]_ B C <-> A. r e. [_ u / y ]_ B A. s e. [_ u / y ]_ B ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
6664, 65sylib 208 . . . . . . . . . . . . . . . 16 |- ( ( A. y e. A Disj x e. B C /\ u e. A ) -> A. r e. [_ u / y ]_ B A. s e. [_ u / y ]_ B ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
6766ad2ant2r 783 . . . . . . . . . . . . . . 15 |- ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) -> A. r e. [_ u / y ]_ B A. s e. [_ u / y ]_ B ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
6867adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) -> A. r e. [_ u / y ]_ B A. s e. [_ u / y ]_ B ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
69 simplrl 800 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) /\ u = v ) -> r e. [_ u / y ]_ B )
70 simplrr 801 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) /\ u = v ) -> s e. [_ v / y ]_ B )
7118adantl 482 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) /\ u = v ) -> [_ u / y ]_ B = [_ v / y ]_ B )
7270, 71eleqtrrd 2704 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) /\ u = v ) -> s e. [_ u / y ]_ B )
7369, 72jca 554 . . . . . . . . . . . . . 14 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) /\ u = v ) -> ( r e. [_ u / y ]_ B /\ s e. [_ u / y ]_ B ) )
74 rsp2 2936 . . . . . . . . . . . . . . 15 |- ( A. r e. [_ u / y ]_ B A. s e. [_ u / y ]_ B ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) -> ( ( r e. [_ u / y ]_ B /\ s e. [_ u / y ]_ B ) -> ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) ) )
7574imp 445 . . . . . . . . . . . . . 14 |- ( ( A. r e. [_ u / y ]_ B A. s e. [_ u / y ]_ B ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ u / y ]_ B ) ) -> ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
7668, 73, 75syl2an2r 876 . . . . . . . . . . . . 13 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) /\ u = v ) -> ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
7776adantlrr 757 . . . . . . . . . . . 12 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) /\ u = v ) -> ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
7877ord 392 . . . . . . . . . . 11 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) /\ u = v ) -> ( -. r = s -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
7960, 78mpd 15 . . . . . . . . . 10 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) /\ u = v ) -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) )
80 ssiun2 4563 . . . . . . . . . . . . . 14 |- ( r e. [_ u / y ]_ B -> [_ r / x ]_ C C_ U_ r e. [_ u / y ]_ B [_ r / x ]_ C )
81 nfcv 2764 . . . . . . . . . . . . . . 15 |- F/_ r C
82 nfcsb1v 3549 . . . . . . . . . . . . . . 15 |- F/_ x [_ r / x ]_ C
83 csbeq1a 3542 . . . . . . . . . . . . . . 15 |- ( x = r -> C = [_ r / x ]_ C )
8481, 82, 83cbviun 4557 . . . . . . . . . . . . . 14 |- U_ x e. [_ u / y ]_ B C = U_ r e. [_ u / y ]_ B [_ r / x ]_ C
8580, 84syl6sseqr 3652 . . . . . . . . . . . . 13 |- ( r e. [_ u / y ]_ B -> [_ r / x ]_ C C_ U_ x e. [_ u / y ]_ B C )
86 ssiun2 4563 . . . . . . . . . . . . . 14 |- ( s e. [_ v / y ]_ B -> [_ s / x ]_ C C_ U_ s e. [_ v / y ]_ B [_ s / x ]_ C )
87 nfcv 2764 . . . . . . . . . . . . . . 15 |- F/_ s C
88 nfcsb1v 3549 . . . . . . . . . . . . . . 15 |- F/_ x [_ s / x ]_ C
89 csbeq1a 3542 . . . . . . . . . . . . . . 15 |- ( x = s -> C = [_ s / x ]_ C )
9087, 88, 89cbviun 4557 . . . . . . . . . . . . . 14 |- U_ x e. [_ v / y ]_ B C = U_ s e. [_ v / y ]_ B [_ s / x ]_ C
9186, 90syl6sseqr 3652 . . . . . . . . . . . . 13 |- ( s e. [_ v / y ]_ B -> [_ s / x ]_ C C_ U_ x e. [_ v / y ]_ B C )
92 ss2in 3840 . . . . . . . . . . . . 13 |- ( ( [_ r / x ]_ C C_ U_ x e. [_ u / y ]_ B C /\ [_ s / x ]_ C C_ U_ x e. [_ v / y ]_ B C ) -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) C_ ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) )
9385, 91, 92syl2an 494 . . . . . . . . . . . 12 |- ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) C_ ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) )
9493ad2antrl 764 . . . . . . . . . . 11 |- ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) C_ ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) )
95 nfcv 2764 . . . . . . . . . . . . . . 15 |- F/_ z U_ x e. B C
96 nfcsb1v 3549 . . . . . . . . . . . . . . . 16 |- F/_ y [_ z / y ]_ B
9796, 2nfiun 4548 . . . . . . . . . . . . . . 15 |- F/_ y U_ x e. [_ z / y ]_ B C
98 csbeq1a 3542 . . . . . . . . . . . . . . . 16 |- ( y = z -> B = [_ z / y ]_ B )
9998iuneq1d 4545 . . . . . . . . . . . . . . 15 |- ( y = z -> U_ x e. B C = U_ x e. [_ z / y ]_ B C )
10095, 97, 99cbvdisj 4630 . . . . . . . . . . . . . 14 |- (Disj y e. A U_ x e. B C <-> Disj z e. A U_ x e. [_ z / y ]_ B C )
101100biimpi 206 . . . . . . . . . . . . 13 |- (Disj y e. A U_ x e. B C -> Disj z e. A U_ x e. [_ z / y ]_ B C )
102101ad3antlr 767 . . . . . . . . . . . 12 |- ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) -> Disj z e. A U_ x e. [_ z / y ]_ B C )
103 simplr 792 . . . . . . . . . . . 12 |- ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) -> ( u e. A /\ v e. A ) )
104 id 22 . . . . . . . . . . . 12 |- ( u =/= v -> u =/= v )
105 csbeq1 3536 . . . . . . . . . . . . . 14 |- ( z = u -> [_ z / y ]_ B = [_ u / y ]_ B )
106105iuneq1d 4545 . . . . . . . . . . . . 13 |- ( z = u -> U_ x e. [_ z / y ]_ B C = U_ x e. [_ u / y ]_ B C )
107 csbeq1 3536 . . . . . . . . . . . . . 14 |- ( z = v -> [_ z / y ]_ B = [_ v / y ]_ B )
108107iuneq1d 4545 . . . . . . . . . . . . 13 |- ( z = v -> U_ x e. [_ z / y ]_ B C = U_ x e. [_ v / y ]_ B C )
109106, 108disji2 4636 . . . . . . . . . . . 12 |- ( (Disj z e. A U_ x e. [_ z / y ]_ B C /\ ( u e. A /\ v e. A ) /\ u =/= v ) -> ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) )
110102, 103, 104, 109syl2an3an 1386 . . . . . . . . . . 11 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) /\ u =/= v ) -> ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) )
111 sseq0 3975 . . . . . . . . . . 11 |- ( ( ( [_ r / x ]_ C i^i [_ s / x ]_ C ) C_ ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) /\ ( U_ x e. [_ u / y ]_ B C i^i U_ x e. [_ v / y ]_ B C ) = (/) ) -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) )
11294, 110, 111syl2an2r 876 . . . . . . . . . 10 |- ( ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) /\ u =/= v ) -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) )
11379, 112pm2.61dane 2881 . . . . . . . . 9 |- ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) /\ -. r = s ) ) -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) )
114113expr 643 . . . . . . . 8 |- ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) -> ( -. r = s -> ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
115114orrd 393 . . . . . . 7 |- ( ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) /\ ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) ) -> ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
116115ex 450 . . . . . 6 |- ( ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) /\ ( u e. A /\ v e. A ) ) -> ( ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) -> ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) ) )
117116rexlimdvva 3038 . . . . 5 |- ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) -> ( E. u e. A E. v e. A ( r e. [_ u / y ]_ B /\ s e. [_ v / y ]_ B ) -> ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) ) )
11859, 117syl5bi 232 . . . 4 |- ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) -> ( ( r e. U_ y e. A B /\ s e. U_ y e. A B ) -> ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) ) )
119118ralrimivv 2970 . . 3 |- ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) -> A. r e. U_ y e. A B A. s e. U_ y e. A B ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
120 disjors 4635 . . 3 |- (Disj x e. U_ y e. A B C <-> A. r e. U_ y e. A B A. s e. U_ y e. A B ( r = s \/ ( [_ r / x ]_ C i^i [_ s / x ]_ C ) = (/) ) )
121119, 120sylibr 224 . 2 |- ( ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) -> Disj x e. U_ y e. A B C )
12246, 121impbid1 215 1 |- (Disj y e. A B -> (Disj x e. U_ y e. A B C <-> ( A. y e. A Disj x e. B C /\ Disj y e. A U_ x e. B C ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   [_csb 3533   i^i cin 3573   C_ wss 3574   (/)c0 3915   U_ciun 4520  Disj wdisj 4620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-iun 4522  df-disj 4621
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator