Metamath Proof Explorer

Theorem disjxun

Description: The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypothesis disjxun.1 
|- ( x = y -> C = D )
Assertion disjxun 
|- ( ( A i^i B ) = (/) -> ( Disj_ x e. ( A u. B ) C <-> ( Disj_ x e. A C /\ Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 disjxun.1 
 |-  ( x = y -> C = D )
2 disjel 
 |-  ( ( ( A i^i B ) = (/) /\ x e. A ) -> -. x e. B )
3 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
4 3 notbid 
 |-  ( x = y -> ( -. x e. B <-> -. y e. B ) )
5 2 4 syl5ibcom 
 |-  ( ( ( A i^i B ) = (/) /\ x e. A ) -> ( x = y -> -. y e. B ) )
6 5 con2d 
 |-  ( ( ( A i^i B ) = (/) /\ x e. A ) -> ( y e. B -> -. x = y ) )
7 6 impr 
 |-  ( ( ( A i^i B ) = (/) /\ ( x e. A /\ y e. B ) ) -> -. x = y )
8 biorf 
 |-  ( -. x = y -> ( ( C i^i D ) = (/) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
9 7 8 syl 
 |-  ( ( ( A i^i B ) = (/) /\ ( x e. A /\ y e. B ) ) -> ( ( C i^i D ) = (/) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
10 9 bicomd 
 |-  ( ( ( A i^i B ) = (/) /\ ( x e. A /\ y e. B ) ) -> ( ( x = y \/ ( C i^i D ) = (/) ) <-> ( C i^i D ) = (/) ) )
11 10 2ralbidva 
 |-  ( ( A i^i B ) = (/) -> ( A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) <-> A. x e. A A. y e. B ( C i^i D ) = (/) ) )
12 11 anbi2d 
 |-  ( ( A i^i B ) = (/) -> ( ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) <-> ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
13 ralunb 
 |-  ( A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) <-> ( A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) )
14 13 ralbii 
 |-  ( A. x e. A A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) <-> A. x e. A ( A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) )
15 nfv 
 |-  F/ z A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) )
16 nfcv 
 |-  F/_ x ( A u. B )
17 nfv 
 |-  F/ x z = w
18 nfcsb1v 
 |-  F/_ x [_ z / x ]_ C
19 nfcsb1v 
 |-  F/_ x [_ w / x ]_ C
20 18 19 nfin 
 |-  F/_ x ( [_ z / x ]_ C i^i [_ w / x ]_ C )
21 20 nfeq1 
 |-  F/ x ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/)
22 17 21 nfor 
 |-  F/ x ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
23 16 22 nfralw 
 |-  F/ x A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) )
24 equequ2 
 |-  ( w = y -> ( x = w <-> x = y ) )
25 nfcv 
 |-  F/_ x y
26 nfcv 
 |-  F/_ x D
27 25 26 1 csbhypf 
 |-  ( w = y -> [_ w / x ]_ C = D )
28 27 ineq2d 
 |-  ( w = y -> ( C i^i [_ w / x ]_ C ) = ( C i^i D ) )
29 28 eqeq1d 
 |-  ( w = y -> ( ( C i^i [_ w / x ]_ C ) = (/) <-> ( C i^i D ) = (/) ) )
30 24 29 orbi12d 
 |-  ( w = y -> ( ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
31 30 cbvralvw 
 |-  ( A. w e. ( A u. B ) ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) )
32 equequ1 
 |-  ( x = z -> ( x = w <-> z = w ) )
33 csbeq1a 
 |-  ( x = z -> C = [_ z / x ]_ C )
34 33 ineq1d 
 |-  ( x = z -> ( C i^i [_ w / x ]_ C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
35 34 eqeq1d 
 |-  ( x = z -> ( ( C i^i [_ w / x ]_ C ) = (/) <-> ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
36 32 35 orbi12d 
 |-  ( x = z -> ( ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
37 36 ralbidv 
 |-  ( x = z -> ( A. w e. ( A u. B ) ( x = w \/ ( C i^i [_ w / x ]_ C ) = (/) ) <-> A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
38 31 37 bitr3id 
 |-  ( x = z -> ( A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) <-> A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
39 15 23 38 cbvralw 
 |-  ( A. x e. A A. y e. ( A u. B ) ( x = y \/ ( C i^i D ) = (/) ) <-> A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
40 r19.26 
 |-  ( A. x e. A ( A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) <-> ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) )
41 14 39 40 3bitr3i 
 |-  ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) ) )
42 1 disjor 
 |-  ( Disj_ x e. A C <-> A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) )
43 42 anbi1i 
 |-  ( ( Disj_ x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( A. x e. A A. y e. A ( x = y \/ ( C i^i D ) = (/) ) /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) )
44 12 41 43 3bitr4g 
 |-  ( ( A i^i B ) = (/) -> ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( Disj_ x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
45 nfv 
 |-  F/ w ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) )
46 equequ2 
 |-  ( x = w -> ( z = x <-> z = w ) )
47 csbeq1a 
 |-  ( x = w -> C = [_ w / x ]_ C )
48 47 ineq2d 
 |-  ( x = w -> ( [_ z / x ]_ C i^i C ) = ( [_ z / x ]_ C i^i [_ w / x ]_ C ) )
49 48 eqeq1d 
 |-  ( x = w -> ( ( [_ z / x ]_ C i^i C ) = (/) <-> ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
50 46 49 orbi12d 
 |-  ( x = w -> ( ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
51 45 22 50 cbvralw 
 |-  ( A. x e. A ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
52 equequ1 
 |-  ( z = y -> ( z = x <-> y = x ) )
53 equcom 
 |-  ( y = x <-> x = y )
54 52 53 bitrdi 
 |-  ( z = y -> ( z = x <-> x = y ) )
55 25 26 1 csbhypf 
 |-  ( z = y -> [_ z / x ]_ C = D )
56 55 ineq1d 
 |-  ( z = y -> ( [_ z / x ]_ C i^i C ) = ( D i^i C ) )
57 incom 
 |-  ( D i^i C ) = ( C i^i D )
58 56 57 eqtrdi 
 |-  ( z = y -> ( [_ z / x ]_ C i^i C ) = ( C i^i D ) )
59 58 eqeq1d 
 |-  ( z = y -> ( ( [_ z / x ]_ C i^i C ) = (/) <-> ( C i^i D ) = (/) ) )
60 54 59 orbi12d 
 |-  ( z = y -> ( ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> ( x = y \/ ( C i^i D ) = (/) ) ) )
61 60 ralbidv 
 |-  ( z = y -> ( A. x e. A ( z = x \/ ( [_ z / x ]_ C i^i C ) = (/) ) <-> A. x e. A ( x = y \/ ( C i^i D ) = (/) ) ) )
62 51 61 bitr3id 
 |-  ( z = y -> ( A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. x e. A ( x = y \/ ( C i^i D ) = (/) ) ) )
63 62 cbvralvw 
 |-  ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. y e. B A. x e. A ( x = y \/ ( C i^i D ) = (/) ) )
64 ralcom 
 |-  ( A. y e. B A. x e. A ( x = y \/ ( C i^i D ) = (/) ) <-> A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) )
65 63 64 bitri 
 |-  ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. x e. A A. y e. B ( x = y \/ ( C i^i D ) = (/) ) )
66 65 11 bitrid 
 |-  ( ( A i^i B ) = (/) -> ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. x e. A A. y e. B ( C i^i D ) = (/) ) )
67 66 anbi1d 
 |-  ( ( A i^i B ) = (/) -> ( ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) <-> ( A. x e. A A. y e. B ( C i^i D ) = (/) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) ) )
68 ralunb 
 |-  ( A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
69 68 ralbii 
 |-  ( A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> A. z e. B ( A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
70 r19.26 
 |-  ( A. z e. B ( A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) <-> ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
71 69 70 bitri 
 |-  ( A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( A. z e. B A. w e. A ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
72 disjors 
 |-  ( Disj_ x e. B C <-> A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
73 72 anbi2ci 
 |-  ( ( Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( A. x e. A A. y e. B ( C i^i D ) = (/) /\ A. z e. B A. w e. B ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
74 67 71 73 3bitr4g 
 |-  ( ( A i^i B ) = (/) -> ( A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
75 44 74 anbi12d 
 |-  ( ( A i^i B ) = (/) -> ( ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) <-> ( ( Disj_ x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) /\ ( Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) ) )
76 disjors 
 |-  ( Disj_ x e. ( A u. B ) C <-> A. z e. ( A u. B ) A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) )
77 ralunb 
 |-  ( A. z e. ( A u. B ) A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) <-> ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
78 76 77 bitri 
 |-  ( Disj_ x e. ( A u. B ) C <-> ( A. z e. A A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) /\ A. z e. B A. w e. ( A u. B ) ( z = w \/ ( [_ z / x ]_ C i^i [_ w / x ]_ C ) = (/) ) ) )
79 df-3an 
 |-  ( ( Disj_ x e. A C /\ Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( ( Disj_ x e. A C /\ Disj_ x e. B C ) /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) )
80 anandir 
 |-  ( ( ( Disj_ x e. A C /\ Disj_ x e. B C ) /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( ( Disj_ x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) /\ ( Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
81 79 80 bitri 
 |-  ( ( Disj_ x e. A C /\ Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) <-> ( ( Disj_ x e. A C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) /\ ( Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )
82 75 78 81 3bitr4g 
 |-  ( ( A i^i B ) = (/) -> ( Disj_ x e. ( A u. B ) C <-> ( Disj_ x e. A C /\ Disj_ x e. B C /\ A. x e. A A. y e. B ( C i^i D ) = (/) ) ) )