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
|
syl5bb |
|- ( ( 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 ) = (/) ) ) ) |