Step |
Hyp |
Ref |
Expression |
1 |
|
dfac5lem.1 |
|- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } |
2 |
|
dfac5lem.2 |
|- B = ( U. A i^i y ) |
3 |
|
dfac5lem.3 |
|- ( ph <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) ) |
4 |
1 2 3
|
dfac5lem4 |
|- ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) ) |
5 |
|
simpr |
|- ( ( w =/= (/) /\ w e. h ) -> w e. h ) |
6 |
5
|
a1i |
|- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> w e. h ) ) |
7 |
|
ineq1 |
|- ( z = ( { w } X. w ) -> ( z i^i y ) = ( ( { w } X. w ) i^i y ) ) |
8 |
7
|
eleq2d |
|- ( z = ( { w } X. w ) -> ( v e. ( z i^i y ) <-> v e. ( ( { w } X. w ) i^i y ) ) ) |
9 |
8
|
eubidv |
|- ( z = ( { w } X. w ) -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( ( { w } X. w ) i^i y ) ) ) |
10 |
9
|
rspccv |
|- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( { w } X. w ) e. A -> E! v v e. ( ( { w } X. w ) i^i y ) ) ) |
11 |
1
|
dfac5lem3 |
|- ( ( { w } X. w ) e. A <-> ( w =/= (/) /\ w e. h ) ) |
12 |
|
dfac5lem1 |
|- ( E! v v e. ( ( { w } X. w ) i^i y ) <-> E! g ( g e. w /\ <. w , g >. e. y ) ) |
13 |
10 11 12
|
3imtr3g |
|- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> E! g ( g e. w /\ <. w , g >. e. y ) ) ) |
14 |
6 13
|
jcad |
|- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> ( w e. h /\ E! g ( g e. w /\ <. w , g >. e. y ) ) ) ) |
15 |
2
|
eleq2i |
|- ( <. w , g >. e. B <-> <. w , g >. e. ( U. A i^i y ) ) |
16 |
|
elin |
|- ( <. w , g >. e. ( U. A i^i y ) <-> ( <. w , g >. e. U. A /\ <. w , g >. e. y ) ) |
17 |
1
|
dfac5lem2 |
|- ( <. w , g >. e. U. A <-> ( w e. h /\ g e. w ) ) |
18 |
17
|
anbi1i |
|- ( ( <. w , g >. e. U. A /\ <. w , g >. e. y ) <-> ( ( w e. h /\ g e. w ) /\ <. w , g >. e. y ) ) |
19 |
|
anass |
|- ( ( ( w e. h /\ g e. w ) /\ <. w , g >. e. y ) <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
20 |
18 19
|
bitri |
|- ( ( <. w , g >. e. U. A /\ <. w , g >. e. y ) <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
21 |
15 16 20
|
3bitri |
|- ( <. w , g >. e. B <-> ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
22 |
21
|
eubii |
|- ( E! g <. w , g >. e. B <-> E! g ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
23 |
|
euanv |
|- ( E! g ( w e. h /\ ( g e. w /\ <. w , g >. e. y ) ) <-> ( w e. h /\ E! g ( g e. w /\ <. w , g >. e. y ) ) ) |
24 |
22 23
|
bitr2i |
|- ( ( w e. h /\ E! g ( g e. w /\ <. w , g >. e. y ) ) <-> E! g <. w , g >. e. B ) |
25 |
14 24
|
syl6ib |
|- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> E! g <. w , g >. e. B ) ) |
26 |
|
euex |
|- ( E! g <. w , g >. e. B -> E. g <. w , g >. e. B ) |
27 |
|
nfeu1 |
|- F/ g E! g <. w , g >. e. B |
28 |
|
nfv |
|- F/ g ( B ` w ) e. w |
29 |
27 28
|
nfim |
|- F/ g ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) |
30 |
21
|
simprbi |
|- ( <. w , g >. e. B -> ( g e. w /\ <. w , g >. e. y ) ) |
31 |
30
|
simpld |
|- ( <. w , g >. e. B -> g e. w ) |
32 |
|
tz6.12 |
|- ( ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) -> ( B ` w ) = g ) |
33 |
32
|
eleq1d |
|- ( ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) -> ( ( B ` w ) e. w <-> g e. w ) ) |
34 |
33
|
biimparc |
|- ( ( g e. w /\ ( <. w , g >. e. B /\ E! g <. w , g >. e. B ) ) -> ( B ` w ) e. w ) |
35 |
34
|
exp32 |
|- ( g e. w -> ( <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) ) ) |
36 |
31 35
|
mpcom |
|- ( <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) ) |
37 |
29 36
|
exlimi |
|- ( E. g <. w , g >. e. B -> ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) ) |
38 |
26 37
|
mpcom |
|- ( E! g <. w , g >. e. B -> ( B ` w ) e. w ) |
39 |
25 38
|
syl6 |
|- ( A. z e. A E! v v e. ( z i^i y ) -> ( ( w =/= (/) /\ w e. h ) -> ( B ` w ) e. w ) ) |
40 |
39
|
expcomd |
|- ( A. z e. A E! v v e. ( z i^i y ) -> ( w e. h -> ( w =/= (/) -> ( B ` w ) e. w ) ) ) |
41 |
40
|
ralrimiv |
|- ( A. z e. A E! v v e. ( z i^i y ) -> A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) ) |
42 |
|
vex |
|- y e. _V |
43 |
42
|
inex2 |
|- ( U. A i^i y ) e. _V |
44 |
2 43
|
eqeltri |
|- B e. _V |
45 |
|
fveq1 |
|- ( f = B -> ( f ` w ) = ( B ` w ) ) |
46 |
45
|
eleq1d |
|- ( f = B -> ( ( f ` w ) e. w <-> ( B ` w ) e. w ) ) |
47 |
46
|
imbi2d |
|- ( f = B -> ( ( w =/= (/) -> ( f ` w ) e. w ) <-> ( w =/= (/) -> ( B ` w ) e. w ) ) ) |
48 |
47
|
ralbidv |
|- ( f = B -> ( A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) <-> A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) ) ) |
49 |
44 48
|
spcev |
|- ( A. w e. h ( w =/= (/) -> ( B ` w ) e. w ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) ) |
50 |
41 49
|
syl |
|- ( A. z e. A E! v v e. ( z i^i y ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) ) |
51 |
50
|
exlimiv |
|- ( E. y A. z e. A E! v v e. ( z i^i y ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) ) |
52 |
4 51
|
syl |
|- ( ph -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) ) |