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 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 )
61 12 2 nfdisjw 
 |-  F/ y Disj_ x e. [_ u / y ]_ B C
62 13 disjeq1d 
 |-  ( y = u -> ( Disj_ x e. B C <-> Disj_ x e. [_ u / y ]_ B C ) )
63 61 62 rspc 
 |-  ( u e. A -> ( A. y e. A Disj_ x e. B C -> Disj_ x e. [_ u / y ]_ B C ) )
64 63 impcom 
 |-  ( ( A. y e. A Disj_ x e. B C /\ u e. A ) -> Disj_ x e. [_ u / y ]_ B C )
65 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 ) = (/) ) )
66 64 65 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 ) = (/) ) )
67 66 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 ) = (/) ) )
68 67 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 ) = (/) ) )
69 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 )
70 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 )
71 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 )
72 70 71 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 )
73 69 72 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 ) )
74 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 ) = (/) ) ) )
75 74 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 ) = (/) ) )
76 68 73 75 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 ) = (/) ) )
77 76 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 ) = (/) ) )
78 77 ord 
 |-  ( ( ( ( ( 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 ) = (/) ) )
79 60 78 mpd 
 |-  ( ( ( ( ( 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 
 |-  ( r e. [_ u / y ]_ B -> [_ r / x ]_ C C_ U_ r e. [_ u / y ]_ B [_ r / x ]_ C )
81 nfcv 
 |-  F/_ r C
82 nfcsb1v 
 |-  F/_ x [_ r / x ]_ C
83 csbeq1a 
 |-  ( x = r -> C = [_ r / x ]_ C )
84 81 82 83 cbviun 
 |-  U_ x e. [_ u / y ]_ B C = U_ r e. [_ u / y ]_ B [_ r / x ]_ C
85 80 84 sseqtrrdi 
 |-  ( r e. [_ u / y ]_ B -> [_ r / x ]_ C C_ U_ x e. [_ u / y ]_ B C )
86 ssiun2 
 |-  ( s e. [_ v / y ]_ B -> [_ s / x ]_ C C_ U_ s e. [_ v / y ]_ B [_ s / x ]_ C )
87 nfcv 
 |-  F/_ s C
88 nfcsb1v 
 |-  F/_ x [_ s / x ]_ C
89 csbeq1a 
 |-  ( x = s -> C = [_ s / x ]_ C )
90 87 88 89 cbviun 
 |-  U_ x e. [_ v / y ]_ B C = U_ s e. [_ v / y ]_ B [_ s / x ]_ C
91 86 90 sseqtrrdi 
 |-  ( s e. [_ v / y ]_ B -> [_ s / x ]_ C C_ U_ x e. [_ v / y ]_ B C )
92 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 ) )
93 85 91 92 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 ) )
94 93 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 ) )
95 nfcv 
 |-  F/_ z U_ x e. B C
96 nfcsb1v 
 |-  F/_ y [_ z / y ]_ B
97 96 2 nfiun 
 |-  F/_ y U_ x e. [_ z / y ]_ B C
98 csbeq1a 
 |-  ( y = z -> B = [_ z / y ]_ B )
99 98 iuneq1d 
 |-  ( y = z -> U_ x e. B C = U_ x e. [_ z / y ]_ B C )
100 95 97 99 cbvdisj 
 |-  ( Disj_ y e. A U_ x e. B C <-> Disj_ z e. A U_ x e. [_ z / y ]_ B C )
101 100 biimpi 
 |-  ( Disj_ y e. A U_ x e. B C -> Disj_ z e. A U_ x e. [_ z / y ]_ B C )
102 101 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 )
103 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 ) )
104 id 
 |-  ( u =/= v -> u =/= v )
105 csbeq1 
 |-  ( z = u -> [_ z / y ]_ B = [_ u / y ]_ B )
106 105 iuneq1d 
 |-  ( z = u -> U_ x e. [_ z / y ]_ B C = U_ x e. [_ u / y ]_ B C )
107 csbeq1 
 |-  ( z = v -> [_ z / y ]_ B = [_ v / y ]_ B )
108 107 iuneq1d 
 |-  ( z = v -> U_ x e. [_ z / y ]_ B C = U_ x e. [_ v / y ]_ B C )
109 106 108 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 ) = (/) )
110 102 103 104 109 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 ) = (/) )
111 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 ) = (/) )
112 94 110 111 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 ) = (/) )
113 79 112 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 ) = (/) )
114 113 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 ) = (/) ) )
115 114 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 ) = (/) ) )
116 115 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 ) = (/) ) ) )
117 116 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 ) = (/) ) ) )
118 59 117 syl5bi 
 |-  ( ( 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 ) = (/) ) ) )
119 118 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 ) = (/) ) )
120 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 ) = (/) ) )
121 119 120 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 )
122 46 121 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 ) ) )