Step |
Hyp |
Ref |
Expression |
1 |
|
fiiuncl.xph |
|- F/ x ph |
2 |
|
fiiuncl.b |
|- ( ( ph /\ x e. A ) -> B e. D ) |
3 |
|
fiiuncl.un |
|- ( ( ph /\ y e. D /\ z e. D ) -> ( y u. z ) e. D ) |
4 |
|
fiiuncl.a |
|- ( ph -> A e. Fin ) |
5 |
|
fiiuncl.n0 |
|- ( ph -> A =/= (/) ) |
6 |
|
neeq1 |
|- ( v = (/) -> ( v =/= (/) <-> (/) =/= (/) ) ) |
7 |
|
iuneq1 |
|- ( v = (/) -> U_ x e. v B = U_ x e. (/) B ) |
8 |
7
|
eleq1d |
|- ( v = (/) -> ( U_ x e. v B e. D <-> U_ x e. (/) B e. D ) ) |
9 |
6 8
|
imbi12d |
|- ( v = (/) -> ( ( v =/= (/) -> U_ x e. v B e. D ) <-> ( (/) =/= (/) -> U_ x e. (/) B e. D ) ) ) |
10 |
|
neeq1 |
|- ( v = w -> ( v =/= (/) <-> w =/= (/) ) ) |
11 |
|
iuneq1 |
|- ( v = w -> U_ x e. v B = U_ x e. w B ) |
12 |
11
|
eleq1d |
|- ( v = w -> ( U_ x e. v B e. D <-> U_ x e. w B e. D ) ) |
13 |
10 12
|
imbi12d |
|- ( v = w -> ( ( v =/= (/) -> U_ x e. v B e. D ) <-> ( w =/= (/) -> U_ x e. w B e. D ) ) ) |
14 |
|
neeq1 |
|- ( v = ( w u. { u } ) -> ( v =/= (/) <-> ( w u. { u } ) =/= (/) ) ) |
15 |
|
iuneq1 |
|- ( v = ( w u. { u } ) -> U_ x e. v B = U_ x e. ( w u. { u } ) B ) |
16 |
15
|
eleq1d |
|- ( v = ( w u. { u } ) -> ( U_ x e. v B e. D <-> U_ x e. ( w u. { u } ) B e. D ) ) |
17 |
14 16
|
imbi12d |
|- ( v = ( w u. { u } ) -> ( ( v =/= (/) -> U_ x e. v B e. D ) <-> ( ( w u. { u } ) =/= (/) -> U_ x e. ( w u. { u } ) B e. D ) ) ) |
18 |
|
neeq1 |
|- ( v = A -> ( v =/= (/) <-> A =/= (/) ) ) |
19 |
|
iuneq1 |
|- ( v = A -> U_ x e. v B = U_ x e. A B ) |
20 |
19
|
eleq1d |
|- ( v = A -> ( U_ x e. v B e. D <-> U_ x e. A B e. D ) ) |
21 |
18 20
|
imbi12d |
|- ( v = A -> ( ( v =/= (/) -> U_ x e. v B e. D ) <-> ( A =/= (/) -> U_ x e. A B e. D ) ) ) |
22 |
|
neirr |
|- -. (/) =/= (/) |
23 |
22
|
pm2.21i |
|- ( (/) =/= (/) -> U_ x e. (/) B e. D ) |
24 |
23
|
a1i |
|- ( ph -> ( (/) =/= (/) -> U_ x e. (/) B e. D ) ) |
25 |
|
iunxun |
|- U_ x e. ( w u. { u } ) B = ( U_ x e. w B u. U_ x e. { u } B ) |
26 |
|
nfcsb1v |
|- F/_ x [_ u / x ]_ B |
27 |
|
vex |
|- u e. _V |
28 |
|
csbeq1a |
|- ( x = u -> B = [_ u / x ]_ B ) |
29 |
26 27 28
|
iunxsnf |
|- U_ x e. { u } B = [_ u / x ]_ B |
30 |
29
|
uneq2i |
|- ( U_ x e. w B u. U_ x e. { u } B ) = ( U_ x e. w B u. [_ u / x ]_ B ) |
31 |
25 30
|
eqtri |
|- U_ x e. ( w u. { u } ) B = ( U_ x e. w B u. [_ u / x ]_ B ) |
32 |
|
iuneq1 |
|- ( w = (/) -> U_ x e. w B = U_ x e. (/) B ) |
33 |
|
0iun |
|- U_ x e. (/) B = (/) |
34 |
33
|
a1i |
|- ( w = (/) -> U_ x e. (/) B = (/) ) |
35 |
32 34
|
eqtrd |
|- ( w = (/) -> U_ x e. w B = (/) ) |
36 |
35
|
uneq1d |
|- ( w = (/) -> ( U_ x e. w B u. [_ u / x ]_ B ) = ( (/) u. [_ u / x ]_ B ) ) |
37 |
|
0un |
|- ( (/) u. [_ u / x ]_ B ) = [_ u / x ]_ B |
38 |
|
unidm |
|- ( [_ u / x ]_ B u. [_ u / x ]_ B ) = [_ u / x ]_ B |
39 |
37 38
|
eqtr4i |
|- ( (/) u. [_ u / x ]_ B ) = ( [_ u / x ]_ B u. [_ u / x ]_ B ) |
40 |
39
|
a1i |
|- ( w = (/) -> ( (/) u. [_ u / x ]_ B ) = ( [_ u / x ]_ B u. [_ u / x ]_ B ) ) |
41 |
36 40
|
eqtrd |
|- ( w = (/) -> ( U_ x e. w B u. [_ u / x ]_ B ) = ( [_ u / x ]_ B u. [_ u / x ]_ B ) ) |
42 |
41
|
adantl |
|- ( ( ( ph /\ u e. ( A \ w ) ) /\ w = (/) ) -> ( U_ x e. w B u. [_ u / x ]_ B ) = ( [_ u / x ]_ B u. [_ u / x ]_ B ) ) |
43 |
|
simpl |
|- ( ( ph /\ u e. ( A \ w ) ) -> ph ) |
44 |
|
eldifi |
|- ( u e. ( A \ w ) -> u e. A ) |
45 |
44
|
adantl |
|- ( ( ph /\ u e. ( A \ w ) ) -> u e. A ) |
46 |
|
nfv |
|- F/ x u e. A |
47 |
1 46
|
nfan |
|- F/ x ( ph /\ u e. A ) |
48 |
|
nfcv |
|- F/_ x D |
49 |
26 48
|
nfel |
|- F/ x [_ u / x ]_ B e. D |
50 |
47 49
|
nfim |
|- F/ x ( ( ph /\ u e. A ) -> [_ u / x ]_ B e. D ) |
51 |
|
eleq1 |
|- ( x = u -> ( x e. A <-> u e. A ) ) |
52 |
51
|
anbi2d |
|- ( x = u -> ( ( ph /\ x e. A ) <-> ( ph /\ u e. A ) ) ) |
53 |
28
|
eleq1d |
|- ( x = u -> ( B e. D <-> [_ u / x ]_ B e. D ) ) |
54 |
52 53
|
imbi12d |
|- ( x = u -> ( ( ( ph /\ x e. A ) -> B e. D ) <-> ( ( ph /\ u e. A ) -> [_ u / x ]_ B e. D ) ) ) |
55 |
50 54 2
|
chvarfv |
|- ( ( ph /\ u e. A ) -> [_ u / x ]_ B e. D ) |
56 |
38 55
|
eqeltrid |
|- ( ( ph /\ u e. A ) -> ( [_ u / x ]_ B u. [_ u / x ]_ B ) e. D ) |
57 |
43 45 56
|
syl2anc |
|- ( ( ph /\ u e. ( A \ w ) ) -> ( [_ u / x ]_ B u. [_ u / x ]_ B ) e. D ) |
58 |
57
|
adantr |
|- ( ( ( ph /\ u e. ( A \ w ) ) /\ w = (/) ) -> ( [_ u / x ]_ B u. [_ u / x ]_ B ) e. D ) |
59 |
42 58
|
eqeltrd |
|- ( ( ( ph /\ u e. ( A \ w ) ) /\ w = (/) ) -> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) |
60 |
59
|
adantlr |
|- ( ( ( ( ph /\ u e. ( A \ w ) ) /\ ( w =/= (/) -> U_ x e. w B e. D ) ) /\ w = (/) ) -> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) |
61 |
|
simplll |
|- ( ( ( ( ph /\ u e. ( A \ w ) ) /\ ( w =/= (/) -> U_ x e. w B e. D ) ) /\ -. w = (/) ) -> ph ) |
62 |
44
|
ad3antlr |
|- ( ( ( ( ph /\ u e. ( A \ w ) ) /\ ( w =/= (/) -> U_ x e. w B e. D ) ) /\ -. w = (/) ) -> u e. A ) |
63 |
|
neqne |
|- ( -. w = (/) -> w =/= (/) ) |
64 |
63
|
adantl |
|- ( ( ( w =/= (/) -> U_ x e. w B e. D ) /\ -. w = (/) ) -> w =/= (/) ) |
65 |
|
simpl |
|- ( ( ( w =/= (/) -> U_ x e. w B e. D ) /\ -. w = (/) ) -> ( w =/= (/) -> U_ x e. w B e. D ) ) |
66 |
64 65
|
mpd |
|- ( ( ( w =/= (/) -> U_ x e. w B e. D ) /\ -. w = (/) ) -> U_ x e. w B e. D ) |
67 |
66
|
adantll |
|- ( ( ( ( ph /\ u e. ( A \ w ) ) /\ ( w =/= (/) -> U_ x e. w B e. D ) ) /\ -. w = (/) ) -> U_ x e. w B e. D ) |
68 |
55
|
3adant3 |
|- ( ( ph /\ u e. A /\ U_ x e. w B e. D ) -> [_ u / x ]_ B e. D ) |
69 |
|
simp3 |
|- ( ( ph /\ u e. A /\ U_ x e. w B e. D ) -> U_ x e. w B e. D ) |
70 |
|
simp1 |
|- ( ( ph /\ u e. A /\ U_ x e. w B e. D ) -> ph ) |
71 |
70 69 68
|
3jca |
|- ( ( ph /\ u e. A /\ U_ x e. w B e. D ) -> ( ph /\ U_ x e. w B e. D /\ [_ u / x ]_ B e. D ) ) |
72 |
|
eleq1 |
|- ( z = [_ u / x ]_ B -> ( z e. D <-> [_ u / x ]_ B e. D ) ) |
73 |
72
|
3anbi3d |
|- ( z = [_ u / x ]_ B -> ( ( ph /\ U_ x e. w B e. D /\ z e. D ) <-> ( ph /\ U_ x e. w B e. D /\ [_ u / x ]_ B e. D ) ) ) |
74 |
|
uneq2 |
|- ( z = [_ u / x ]_ B -> ( U_ x e. w B u. z ) = ( U_ x e. w B u. [_ u / x ]_ B ) ) |
75 |
74
|
eleq1d |
|- ( z = [_ u / x ]_ B -> ( ( U_ x e. w B u. z ) e. D <-> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) ) |
76 |
73 75
|
imbi12d |
|- ( z = [_ u / x ]_ B -> ( ( ( ph /\ U_ x e. w B e. D /\ z e. D ) -> ( U_ x e. w B u. z ) e. D ) <-> ( ( ph /\ U_ x e. w B e. D /\ [_ u / x ]_ B e. D ) -> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) ) ) |
77 |
76
|
imbi2d |
|- ( z = [_ u / x ]_ B -> ( ( U_ x e. w B e. D -> ( ( ph /\ U_ x e. w B e. D /\ z e. D ) -> ( U_ x e. w B u. z ) e. D ) ) <-> ( U_ x e. w B e. D -> ( ( ph /\ U_ x e. w B e. D /\ [_ u / x ]_ B e. D ) -> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) ) ) ) |
78 |
|
eleq1 |
|- ( y = U_ x e. w B -> ( y e. D <-> U_ x e. w B e. D ) ) |
79 |
78
|
3anbi2d |
|- ( y = U_ x e. w B -> ( ( ph /\ y e. D /\ z e. D ) <-> ( ph /\ U_ x e. w B e. D /\ z e. D ) ) ) |
80 |
|
uneq1 |
|- ( y = U_ x e. w B -> ( y u. z ) = ( U_ x e. w B u. z ) ) |
81 |
80
|
eleq1d |
|- ( y = U_ x e. w B -> ( ( y u. z ) e. D <-> ( U_ x e. w B u. z ) e. D ) ) |
82 |
79 81
|
imbi12d |
|- ( y = U_ x e. w B -> ( ( ( ph /\ y e. D /\ z e. D ) -> ( y u. z ) e. D ) <-> ( ( ph /\ U_ x e. w B e. D /\ z e. D ) -> ( U_ x e. w B u. z ) e. D ) ) ) |
83 |
82 3
|
vtoclg |
|- ( U_ x e. w B e. D -> ( ( ph /\ U_ x e. w B e. D /\ z e. D ) -> ( U_ x e. w B u. z ) e. D ) ) |
84 |
77 83
|
vtoclg |
|- ( [_ u / x ]_ B e. D -> ( U_ x e. w B e. D -> ( ( ph /\ U_ x e. w B e. D /\ [_ u / x ]_ B e. D ) -> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) ) ) |
85 |
68 69 71 84
|
syl3c |
|- ( ( ph /\ u e. A /\ U_ x e. w B e. D ) -> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) |
86 |
61 62 67 85
|
syl3anc |
|- ( ( ( ( ph /\ u e. ( A \ w ) ) /\ ( w =/= (/) -> U_ x e. w B e. D ) ) /\ -. w = (/) ) -> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) |
87 |
60 86
|
pm2.61dan |
|- ( ( ( ph /\ u e. ( A \ w ) ) /\ ( w =/= (/) -> U_ x e. w B e. D ) ) -> ( U_ x e. w B u. [_ u / x ]_ B ) e. D ) |
88 |
31 87
|
eqeltrid |
|- ( ( ( ph /\ u e. ( A \ w ) ) /\ ( w =/= (/) -> U_ x e. w B e. D ) ) -> U_ x e. ( w u. { u } ) B e. D ) |
89 |
88
|
a1d |
|- ( ( ( ph /\ u e. ( A \ w ) ) /\ ( w =/= (/) -> U_ x e. w B e. D ) ) -> ( ( w u. { u } ) =/= (/) -> U_ x e. ( w u. { u } ) B e. D ) ) |
90 |
89
|
ex |
|- ( ( ph /\ u e. ( A \ w ) ) -> ( ( w =/= (/) -> U_ x e. w B e. D ) -> ( ( w u. { u } ) =/= (/) -> U_ x e. ( w u. { u } ) B e. D ) ) ) |
91 |
90
|
adantrl |
|- ( ( ph /\ ( w C_ A /\ u e. ( A \ w ) ) ) -> ( ( w =/= (/) -> U_ x e. w B e. D ) -> ( ( w u. { u } ) =/= (/) -> U_ x e. ( w u. { u } ) B e. D ) ) ) |
92 |
9 13 17 21 24 91 4
|
findcard2d |
|- ( ph -> ( A =/= (/) -> U_ x e. A B e. D ) ) |
93 |
5 92
|
mpd |
|- ( ph -> U_ x e. A B e. D ) |