Step |
Hyp |
Ref |
Expression |
1 |
|
dfac4 |
|- ( CHOICE <-> A. x E. f ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) ) |
2 |
|
neeq1 |
|- ( z = w -> ( z =/= (/) <-> w =/= (/) ) ) |
3 |
2
|
cbvralvw |
|- ( A. z e. x z =/= (/) <-> A. w e. x w =/= (/) ) |
4 |
3
|
anbi2i |
|- ( ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. z e. x z =/= (/) ) <-> ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. w e. x w =/= (/) ) ) |
5 |
|
r19.26 |
|- ( A. w e. x ( ( w =/= (/) -> ( f ` w ) e. w ) /\ w =/= (/) ) <-> ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. w e. x w =/= (/) ) ) |
6 |
4 5
|
bitr4i |
|- ( ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. z e. x z =/= (/) ) <-> A. w e. x ( ( w =/= (/) -> ( f ` w ) e. w ) /\ w =/= (/) ) ) |
7 |
|
pm3.35 |
|- ( ( w =/= (/) /\ ( w =/= (/) -> ( f ` w ) e. w ) ) -> ( f ` w ) e. w ) |
8 |
7
|
ancoms |
|- ( ( ( w =/= (/) -> ( f ` w ) e. w ) /\ w =/= (/) ) -> ( f ` w ) e. w ) |
9 |
8
|
ralimi |
|- ( A. w e. x ( ( w =/= (/) -> ( f ` w ) e. w ) /\ w =/= (/) ) -> A. w e. x ( f ` w ) e. w ) |
10 |
6 9
|
sylbi |
|- ( ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. z e. x z =/= (/) ) -> A. w e. x ( f ` w ) e. w ) |
11 |
|
r19.26 |
|- ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( A. w e. x ( f ` w ) e. w /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) ) |
12 |
|
elin |
|- ( v e. ( z i^i ran f ) <-> ( v e. z /\ v e. ran f ) ) |
13 |
|
fvelrnb |
|- ( f Fn x -> ( v e. ran f <-> E. t e. x ( f ` t ) = v ) ) |
14 |
13
|
biimpac |
|- ( ( v e. ran f /\ f Fn x ) -> E. t e. x ( f ` t ) = v ) |
15 |
|
fveq2 |
|- ( w = t -> ( f ` w ) = ( f ` t ) ) |
16 |
|
id |
|- ( w = t -> w = t ) |
17 |
15 16
|
eleq12d |
|- ( w = t -> ( ( f ` w ) e. w <-> ( f ` t ) e. t ) ) |
18 |
|
neeq2 |
|- ( w = t -> ( z =/= w <-> z =/= t ) ) |
19 |
|
ineq2 |
|- ( w = t -> ( z i^i w ) = ( z i^i t ) ) |
20 |
19
|
eqeq1d |
|- ( w = t -> ( ( z i^i w ) = (/) <-> ( z i^i t ) = (/) ) ) |
21 |
18 20
|
imbi12d |
|- ( w = t -> ( ( z =/= w -> ( z i^i w ) = (/) ) <-> ( z =/= t -> ( z i^i t ) = (/) ) ) ) |
22 |
17 21
|
anbi12d |
|- ( w = t -> ( ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) ) ) |
23 |
22
|
rspcv |
|- ( t e. x -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) ) ) |
24 |
|
minel |
|- ( ( ( f ` t ) e. t /\ ( z i^i t ) = (/) ) -> -. ( f ` t ) e. z ) |
25 |
24
|
ex |
|- ( ( f ` t ) e. t -> ( ( z i^i t ) = (/) -> -. ( f ` t ) e. z ) ) |
26 |
25
|
imim2d |
|- ( ( f ` t ) e. t -> ( ( z =/= t -> ( z i^i t ) = (/) ) -> ( z =/= t -> -. ( f ` t ) e. z ) ) ) |
27 |
26
|
imp |
|- ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) -> ( z =/= t -> -. ( f ` t ) e. z ) ) |
28 |
27
|
necon4ad |
|- ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) -> ( ( f ` t ) e. z -> z = t ) ) |
29 |
|
eleq1 |
|- ( ( f ` t ) = v -> ( ( f ` t ) e. z <-> v e. z ) ) |
30 |
29
|
biimpar |
|- ( ( ( f ` t ) = v /\ v e. z ) -> ( f ` t ) e. z ) |
31 |
28 30
|
impel |
|- ( ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) /\ ( ( f ` t ) = v /\ v e. z ) ) -> z = t ) |
32 |
|
fveq2 |
|- ( z = t -> ( f ` z ) = ( f ` t ) ) |
33 |
|
eqeq2 |
|- ( ( f ` t ) = v -> ( ( f ` z ) = ( f ` t ) <-> ( f ` z ) = v ) ) |
34 |
|
eqcom |
|- ( ( f ` z ) = v <-> v = ( f ` z ) ) |
35 |
33 34
|
bitrdi |
|- ( ( f ` t ) = v -> ( ( f ` z ) = ( f ` t ) <-> v = ( f ` z ) ) ) |
36 |
32 35
|
syl5ib |
|- ( ( f ` t ) = v -> ( z = t -> v = ( f ` z ) ) ) |
37 |
36
|
ad2antrl |
|- ( ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) /\ ( ( f ` t ) = v /\ v e. z ) ) -> ( z = t -> v = ( f ` z ) ) ) |
38 |
31 37
|
mpd |
|- ( ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) /\ ( ( f ` t ) = v /\ v e. z ) ) -> v = ( f ` z ) ) |
39 |
38
|
exp32 |
|- ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) -> ( ( f ` t ) = v -> ( v e. z -> v = ( f ` z ) ) ) ) |
40 |
23 39
|
syl6com |
|- ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( t e. x -> ( ( f ` t ) = v -> ( v e. z -> v = ( f ` z ) ) ) ) ) |
41 |
40
|
com14 |
|- ( v e. z -> ( t e. x -> ( ( f ` t ) = v -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> v = ( f ` z ) ) ) ) ) |
42 |
41
|
rexlimdv |
|- ( v e. z -> ( E. t e. x ( f ` t ) = v -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> v = ( f ` z ) ) ) ) |
43 |
14 42
|
syl5 |
|- ( v e. z -> ( ( v e. ran f /\ f Fn x ) -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> v = ( f ` z ) ) ) ) |
44 |
43
|
expd |
|- ( v e. z -> ( v e. ran f -> ( f Fn x -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> v = ( f ` z ) ) ) ) ) |
45 |
44
|
com4t |
|- ( f Fn x -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v e. z -> ( v e. ran f -> v = ( f ` z ) ) ) ) ) |
46 |
45
|
imp4b |
|- ( ( f Fn x /\ A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) ) -> ( ( v e. z /\ v e. ran f ) -> v = ( f ` z ) ) ) |
47 |
12 46
|
syl5bi |
|- ( ( f Fn x /\ A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) ) -> ( v e. ( z i^i ran f ) -> v = ( f ` z ) ) ) |
48 |
11 47
|
sylan2br |
|- ( ( f Fn x /\ ( A. w e. x ( f ` w ) e. w /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) ) -> ( v e. ( z i^i ran f ) -> v = ( f ` z ) ) ) |
49 |
48
|
anassrs |
|- ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v e. ( z i^i ran f ) -> v = ( f ` z ) ) ) |
50 |
49
|
adantlr |
|- ( ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v e. ( z i^i ran f ) -> v = ( f ` z ) ) ) |
51 |
|
fveq2 |
|- ( w = z -> ( f ` w ) = ( f ` z ) ) |
52 |
|
id |
|- ( w = z -> w = z ) |
53 |
51 52
|
eleq12d |
|- ( w = z -> ( ( f ` w ) e. w <-> ( f ` z ) e. z ) ) |
54 |
53
|
rspcv |
|- ( z e. x -> ( A. w e. x ( f ` w ) e. w -> ( f ` z ) e. z ) ) |
55 |
|
fnfvelrn |
|- ( ( f Fn x /\ z e. x ) -> ( f ` z ) e. ran f ) |
56 |
55
|
expcom |
|- ( z e. x -> ( f Fn x -> ( f ` z ) e. ran f ) ) |
57 |
54 56
|
anim12d |
|- ( z e. x -> ( ( A. w e. x ( f ` w ) e. w /\ f Fn x ) -> ( ( f ` z ) e. z /\ ( f ` z ) e. ran f ) ) ) |
58 |
|
elin |
|- ( ( f ` z ) e. ( z i^i ran f ) <-> ( ( f ` z ) e. z /\ ( f ` z ) e. ran f ) ) |
59 |
57 58
|
syl6ibr |
|- ( z e. x -> ( ( A. w e. x ( f ` w ) e. w /\ f Fn x ) -> ( f ` z ) e. ( z i^i ran f ) ) ) |
60 |
59
|
expd |
|- ( z e. x -> ( A. w e. x ( f ` w ) e. w -> ( f Fn x -> ( f ` z ) e. ( z i^i ran f ) ) ) ) |
61 |
60
|
com13 |
|- ( f Fn x -> ( A. w e. x ( f ` w ) e. w -> ( z e. x -> ( f ` z ) e. ( z i^i ran f ) ) ) ) |
62 |
61
|
imp31 |
|- ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( f ` z ) e. ( z i^i ran f ) ) |
63 |
|
eleq1 |
|- ( v = ( f ` z ) -> ( v e. ( z i^i ran f ) <-> ( f ` z ) e. ( z i^i ran f ) ) ) |
64 |
62 63
|
syl5ibrcom |
|- ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( v = ( f ` z ) -> v e. ( z i^i ran f ) ) ) |
65 |
64
|
adantr |
|- ( ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v = ( f ` z ) -> v e. ( z i^i ran f ) ) ) |
66 |
50 65
|
impbid |
|- ( ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) |
67 |
66
|
ex |
|- ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) ) |
68 |
67
|
alrimdv |
|- ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. v ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) ) |
69 |
|
fvex |
|- ( f ` z ) e. _V |
70 |
|
eqeq2 |
|- ( h = ( f ` z ) -> ( v = h <-> v = ( f ` z ) ) ) |
71 |
70
|
bibi2d |
|- ( h = ( f ` z ) -> ( ( v e. ( z i^i ran f ) <-> v = h ) <-> ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) ) |
72 |
71
|
albidv |
|- ( h = ( f ` z ) -> ( A. v ( v e. ( z i^i ran f ) <-> v = h ) <-> A. v ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) ) |
73 |
69 72
|
spcev |
|- ( A. v ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) -> E. h A. v ( v e. ( z i^i ran f ) <-> v = h ) ) |
74 |
|
eu6 |
|- ( E! v v e. ( z i^i ran f ) <-> E. h A. v ( v e. ( z i^i ran f ) <-> v = h ) ) |
75 |
73 74
|
sylibr |
|- ( A. v ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) -> E! v v e. ( z i^i ran f ) ) |
76 |
68 75
|
syl6 |
|- ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E! v v e. ( z i^i ran f ) ) ) |
77 |
76
|
ralimdva |
|- ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) ) |
78 |
77
|
ex |
|- ( f Fn x -> ( A. w e. x ( f ` w ) e. w -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) ) ) |
79 |
10 78
|
syl5 |
|- ( f Fn x -> ( ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. z e. x z =/= (/) ) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) ) ) |
80 |
79
|
expd |
|- ( f Fn x -> ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) -> ( A. z e. x z =/= (/) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) ) ) ) |
81 |
80
|
imp4b |
|- ( ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) ) |
82 |
|
vex |
|- f e. _V |
83 |
82
|
rnex |
|- ran f e. _V |
84 |
|
ineq2 |
|- ( y = ran f -> ( z i^i y ) = ( z i^i ran f ) ) |
85 |
84
|
eleq2d |
|- ( y = ran f -> ( v e. ( z i^i y ) <-> v e. ( z i^i ran f ) ) ) |
86 |
85
|
eubidv |
|- ( y = ran f -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( z i^i ran f ) ) ) |
87 |
86
|
ralbidv |
|- ( y = ran f -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x E! v v e. ( z i^i ran f ) ) ) |
88 |
83 87
|
spcev |
|- ( A. z e. x E! v v e. ( z i^i ran f ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) |
89 |
81 88
|
syl6 |
|- ( ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) -> ( ( 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 ) ) ) |
90 |
89
|
exlimiv |
|- ( E. f ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) -> ( ( 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 ) ) ) |
91 |
90
|
alimi |
|- ( A. x E. f ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) -> 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 ) ) ) |
92 |
1 91
|
sylbi |
|- ( CHOICE -> 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 ) ) ) |
93 |
|
eqid |
|- { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } |
94 |
|
eqid |
|- ( U. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } i^i y ) = ( U. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } i^i y ) |
95 |
|
biid |
|- ( 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 ) ) <-> 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 ) ) ) |
96 |
93 94 95
|
dfac5lem5 |
|- ( 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 ) ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) ) |
97 |
96
|
alrimiv |
|- ( 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 ) ) -> A. h E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) ) |
98 |
|
dfac3 |
|- ( CHOICE <-> A. h E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) ) |
99 |
97 98
|
sylibr |
|- ( 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 ) ) -> CHOICE ) |
100 |
92 99
|
impbii |
|- ( CHOICE <-> 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 ) ) ) |