Metamath Proof Explorer

Theorem disjxiun

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)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 nfiu1 
 |-  F/_ y U_ y e. A B
2 nfcv 
 |-  F/_ y C
3 1 2 nfdisjw 
 |-  F/ y Disj_ x e. U_ y e. A B C
4 disjss1 
 |-  ( B C_ U_ y e. A B -> ( Disj_ x e. U_ y e. A B C -> Disj_ x e. B C ) )
5 ssiun2 
 |-  ( y e. A -> B C_ U_ y e. A B )
6 4 5 syl11 
 |-  ( Disj_ x e. U_ y e. A B C -> ( y e. A -> Disj_ x e. B C ) )
7 3 6 ralrimi 
 |-  ( Disj_ x e. U_ y e. A B C -> A. y e. A Disj_ x e. B C )
8 7 a1i 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( u e. A -> [_ u / y ]_ B C_ U_ u e. A [_ u / y ]_ B )
11 nfcv 
 |-  F/_ u B
12 nfcsb1v 
 |-  F/_ y [_ u / y ]_ B
13 csbeq1a 
 |-  ( y = u -> B = [_ u / y ]_ B )
14 11 12 13 cbviun 
 |-  U_ y e. A B = U_ u e. A [_ u / y ]_ B
15 10 14 sseqtrrdi 
 |-  ( u e. A -> [_ u / y ]_ B C_ U_ y e. A B )
16 15 adantr 
 |-  ( ( u e. A /\ v e. A ) -> [_ u / y ]_ B C_ U_ y e. A B )
17 16 ad2antrl 
 |-  ( ( ( 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 
 |-  ( u = v -> [_ u / y ]_ B = [_ v / y ]_ B )
19 18 sseq1d 
 |-  ( u = v -> ( [_ u / y ]_ B C_ U_ y e. A B <-> [_ v / y ]_ B C_ U_ y e. A B ) )
20 19 15 vtoclga 
 |-  ( v e. A -> [_ v / y ]_ B C_ U_ y e. A B )
21 20 adantl 
 |-  ( ( u e. A /\ v e. A ) -> [_ v / y ]_ B C_ U_ y e. A B )
22 21 ad2antrl 
 |-  ( ( ( 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 )
23 11 12 13 cbvdisj 
 |-  ( Disj_ y e. A B <-> Disj_ u e. A [_ u / y ]_ B )
24 18 disjor 
 |-  ( 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 ) = (/) ) )
25 23 24 sylbb 
 |-  ( 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 
 |-  ( 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 ) = (/) ) ) )
27 25 26 syl 
 |-  ( Disj_ y e. A B -> ( ( u e. A /\ v e. A ) -> ( u = v \/ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) ) )
28 27 imp 
 |-  ( ( Disj_ y e. A B /\ ( u e. A /\ v e. A ) ) -> ( u = v \/ ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) )
29 28 ord 
 |-  ( ( Disj_ y e. A B /\ ( u e. A /\ v e. A ) ) -> ( -. u = v -> ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) ) )
30 29 impr 
 |-  ( ( Disj_ y e. A B /\ ( ( u e. A /\ v e. A ) /\ -. u = v ) ) -> ( [_ u / y ]_ B i^i [_ v / y ]_ B ) = (/) )
31 30 adantlr 
 |-  ( ( ( 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 
 |-  ( ( 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 ) = (/) )
33 9 17 22 31 32 syl13anc 
 |-  ( ( ( 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 ) = (/) )
34 33 expr 
 |-  ( ( ( 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 ) = (/) ) )
35 34 orrd 
 |-  ( ( ( 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 ) = (/) ) )
36 35 ralrimivva 
 |-  ( ( 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 ) = (/) ) )
37 18 iuneq1d 
 |-  ( u = v -> U_ x e. [_ u / y ]_ B C = U_ x e. [_ v / y ]_ B C )
38 37 disjor 
 |-  ( 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 ) = (/) ) )
39 36 38 sylibr 
 |-  ( ( 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 
 |-  F/_ u U_ x e. B C
41 12 2 nfiun 
 |-  F/_ y U_ x e. [_ u / y ]_ B C
42 13 iuneq1d 
 |-  ( y = u -> U_ x e. B C = U_ x e. [_ u / y ]_ B C )
43 40 41 42 cbvdisj 
 |-  ( Disj_ y e. A U_ x e. B C <-> Disj_ u e. A U_ x e. [_ u / y ]_ B C )
44 39 43 sylibr 
 |-  ( ( Disj_ y e. A B /\ Disj_ x e. U_ y e. A B C ) -> Disj_ y e. A U_ x e. B C )
45 44 ex 
 |-  ( Disj_ y e. A B -> ( Disj_ x e. U_ y e. A B C -> Disj_ y e. A U_ x e. B C ) )
46 8 45 jcad 
 |-  ( 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 ) ) )
47 14 eleq2i 
 |-  ( r e. U_ y e. A B <-> r e. U_ u e. A [_ u / y ]_ B )
48 eliun 
 |-  ( r e. U_ u e. A [_ u / y ]_ B <-> E. u e. A r e. [_ u / y ]_ B )
49 47 48 bitri 
 |-  ( r e. U_ y e. A B <-> E. u e. A r e. [_ u / y ]_ B )
50 nfcv 
 |-  F/_ v B
51 nfcsb1v 
 |-  F/_ y [_ v / y ]_ B
52 csbeq1a 
 |-  ( y = v -> B = [_ v / y ]_ B )
53 50 51 52 cbviun 
 |-  U_ y e. A B = U_ v e. A [_ v / y ]_ B
54 53 eleq2i 
 |-  ( s e. U_ y e. A B <-> s e. U_ v e. A [_ v / y ]_ B )
55 eliun 
 |-  ( s e. U_ v e. A [_ v / y ]_ B <-> E. v e. A s e. [_ v / y ]_ B )
56 54 55 bitri 
 |-  ( s e. U_ y e. A B <-> E. v e. A s e. [_ v / y ]_ B )
57 49 56 anbi12i 
 |-  ( ( 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 
 |-  ( 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 ) )
59 57 58 bitr4i 
 |-  ( ( 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 12 2 nfdisjw 
 |-  F/ y Disj_ x e. [_ u / y ]_ B C
61 13 disjeq1d 
 |-  ( y = u -> ( Disj_ x e. B C <-> Disj_ x e. [_ u / y ]_ B C ) )
62 60 61 rspc 
 |-  ( u e. A -> ( A. y e. A Disj_ x e. B C -> Disj_ x e. [_ u / y ]_ B C ) )
63 62 impcom 
 |-  ( ( A. y e. A Disj_ x e. B C /\ u e. A ) -> Disj_ x e. [_ u / y ]_ B C )
64 disjors 
 |-  ( 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 ) = (/) ) )
65 63 64 sylib 
 |-  ( ( 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 ) = (/) ) )
66 65 ad2ant2r 
 |-  ( ( ( 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 ) = (/) ) )
67 66 adantr 
 |-  ( ( ( ( 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 ) = (/) ) )
68 simplrl 
 |-  ( ( ( ( ( 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 )
69 simplrr 
 |-  ( ( ( ( ( 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 )
70 18 adantl 
 |-  ( ( ( ( ( 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 )
71 69 70 eleqtrrd 
 |-  ( ( ( ( ( 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 )
72 68 71 jca 
 |-  ( ( ( ( ( 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 ) )
73 rsp2 
 |-  ( 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 ) = (/) ) ) )
74 73 imp 
 |-  ( ( 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 ) = (/) ) )
75 67 72 74 syl2an2r 
 |-  ( ( ( ( ( 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 ) = (/) ) )
76 75 adantlrr 
 |-  ( ( ( ( ( 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 ) = (/) ) )
77 simplrr 
 |-  ( ( ( ( ( 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 )
78 76 77 orcnd 
 |-  ( ( ( ( ( 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 ) = (/) )
79 ssiun2 
 |-  ( r e. [_ u / y ]_ B -> [_ r / x ]_ C C_ U_ r e. [_ u / y ]_ B [_ r / x ]_ C )
80 nfcv 
 |-  F/_ r C
81 nfcsb1v 
 |-  F/_ x [_ r / x ]_ C
82 csbeq1a 
 |-  ( x = r -> C = [_ r / x ]_ C )
83 80 81 82 cbviun 
 |-  U_ x e. [_ u / y ]_ B C = U_ r e. [_ u / y ]_ B [_ r / x ]_ C
84 79 83 sseqtrrdi 
 |-  ( r e. [_ u / y ]_ B -> [_ r / x ]_ C C_ U_ x e. [_ u / y ]_ B C )
85 ssiun2 
 |-  ( s e. [_ v / y ]_ B -> [_ s / x ]_ C C_ U_ s e. [_ v / y ]_ B [_ s / x ]_ C )
86 nfcv 
 |-  F/_ s C
87 nfcsb1v 
 |-  F/_ x [_ s / x ]_ C
88 csbeq1a 
 |-  ( x = s -> C = [_ s / x ]_ C )
89 86 87 88 cbviun 
 |-  U_ x e. [_ v / y ]_ B C = U_ s e. [_ v / y ]_ B [_ s / x ]_ C
90 85 89 sseqtrrdi 
 |-  ( s e. [_ v / y ]_ B -> [_ s / x ]_ C C_ U_ x e. [_ v / y ]_ B C )
91 ss2in 
 |-  ( ( [_ 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 ) )
92 84 90 91 syl2an 
 |-  ( ( 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 ) )
93 92 ad2antrl 
 |-  ( ( ( ( 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 ) )
94 nfcv 
 |-  F/_ z U_ x e. B C
95 nfcsb1v 
 |-  F/_ y [_ z / y ]_ B
96 95 2 nfiun 
 |-  F/_ y U_ x e. [_ z / y ]_ B C
97 csbeq1a 
 |-  ( y = z -> B = [_ z / y ]_ B )
98 97 iuneq1d 
 |-  ( y = z -> U_ x e. B C = U_ x e. [_ z / y ]_ B C )
99 94 96 98 cbvdisj 
 |-  ( Disj_ y e. A U_ x e. B C <-> Disj_ z e. A U_ x e. [_ z / y ]_ B C )
100 99 biimpi 
 |-  ( Disj_ y e. A U_ x e. B C -> Disj_ z e. A U_ x e. [_ z / y ]_ B C )
101 100 ad3antlr 
 |-  ( ( ( ( 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 )
102 simplr 
 |-  ( ( ( ( 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 ) )
103 id 
 |-  ( u =/= v -> u =/= v )
104 csbeq1 
 |-  ( z = u -> [_ z / y ]_ B = [_ u / y ]_ B )
105 104 iuneq1d 
 |-  ( z = u -> U_ x e. [_ z / y ]_ B C = U_ x e. [_ u / y ]_ B C )
106 csbeq1 
 |-  ( z = v -> [_ z / y ]_ B = [_ v / y ]_ B )
107 106 iuneq1d 
 |-  ( z = v -> U_ x e. [_ z / y ]_ B C = U_ x e. [_ v / y ]_ B C )
108 105 107 disji2 
 |-  ( ( 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 ) = (/) )
109 101 102 103 108 syl2an3an 
 |-  ( ( ( ( ( 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 ) = (/) )
110 sseq0 
 |-  ( ( ( [_ 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 ) = (/) )
111 93 109 110 syl2an2r 
 |-  ( ( ( ( ( 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 ) = (/) )
112 78 111 pm2.61dane 
 |-  ( ( ( ( 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 ) = (/) )
113 112 expr 
 |-  ( ( ( ( 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 ) = (/) ) )
114 113 orrd 
 |-  ( ( ( ( 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 ) = (/) ) )
115 114 ex 
 |-  ( ( ( 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 ) = (/) ) ) )
116 115 rexlimdvva 
 |-  ( ( 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 ) = (/) ) ) )
117 59 116 biimtrid 
 |-  ( ( 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 ) = (/) ) ) )
118 117 ralrimivv 
 |-  ( ( 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 ) = (/) ) )
119 disjors 
 |-  ( 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 ) = (/) ) )
120 118 119 sylibr 
 |-  ( ( 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 )
121 46 120 impbid1 
 |-  ( 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 ) ) )