Step |
Hyp |
Ref |
Expression |
1 |
|
df-ac |
|- ( CHOICE <-> A. y E. f ( f C_ y /\ f Fn dom y ) ) |
2 |
|
vex |
|- x e. _V |
3 |
|
vuniex |
|- U. x e. _V |
4 |
2 3
|
xpex |
|- ( x X. U. x ) e. _V |
5 |
|
simpl |
|- ( ( w e. x /\ v e. w ) -> w e. x ) |
6 |
|
elunii |
|- ( ( v e. w /\ w e. x ) -> v e. U. x ) |
7 |
6
|
ancoms |
|- ( ( w e. x /\ v e. w ) -> v e. U. x ) |
8 |
5 7
|
jca |
|- ( ( w e. x /\ v e. w ) -> ( w e. x /\ v e. U. x ) ) |
9 |
8
|
ssopab2i |
|- { <. w , v >. | ( w e. x /\ v e. w ) } C_ { <. w , v >. | ( w e. x /\ v e. U. x ) } |
10 |
|
df-xp |
|- ( x X. U. x ) = { <. w , v >. | ( w e. x /\ v e. U. x ) } |
11 |
9 10
|
sseqtrri |
|- { <. w , v >. | ( w e. x /\ v e. w ) } C_ ( x X. U. x ) |
12 |
4 11
|
ssexi |
|- { <. w , v >. | ( w e. x /\ v e. w ) } e. _V |
13 |
|
sseq2 |
|- ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( f C_ y <-> f C_ { <. w , v >. | ( w e. x /\ v e. w ) } ) ) |
14 |
|
dmeq |
|- ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> dom y = dom { <. w , v >. | ( w e. x /\ v e. w ) } ) |
15 |
14
|
fneq2d |
|- ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( f Fn dom y <-> f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) ) |
16 |
13 15
|
anbi12d |
|- ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( ( f C_ y /\ f Fn dom y ) <-> ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) ) ) |
17 |
16
|
exbidv |
|- ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( E. f ( f C_ y /\ f Fn dom y ) <-> E. f ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) ) ) |
18 |
12 17
|
spcv |
|- ( A. y E. f ( f C_ y /\ f Fn dom y ) -> E. f ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) ) |
19 |
|
fndm |
|- ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> dom f = dom { <. w , v >. | ( w e. x /\ v e. w ) } ) |
20 |
|
dmopab |
|- dom { <. w , v >. | ( w e. x /\ v e. w ) } = { w | E. v ( w e. x /\ v e. w ) } |
21 |
20
|
eleq2i |
|- ( z e. dom { <. w , v >. | ( w e. x /\ v e. w ) } <-> z e. { w | E. v ( w e. x /\ v e. w ) } ) |
22 |
|
vex |
|- z e. _V |
23 |
|
elequ1 |
|- ( w = z -> ( w e. x <-> z e. x ) ) |
24 |
|
eleq2 |
|- ( w = z -> ( v e. w <-> v e. z ) ) |
25 |
23 24
|
anbi12d |
|- ( w = z -> ( ( w e. x /\ v e. w ) <-> ( z e. x /\ v e. z ) ) ) |
26 |
25
|
exbidv |
|- ( w = z -> ( E. v ( w e. x /\ v e. w ) <-> E. v ( z e. x /\ v e. z ) ) ) |
27 |
22 26
|
elab |
|- ( z e. { w | E. v ( w e. x /\ v e. w ) } <-> E. v ( z e. x /\ v e. z ) ) |
28 |
|
19.42v |
|- ( E. v ( z e. x /\ v e. z ) <-> ( z e. x /\ E. v v e. z ) ) |
29 |
|
n0 |
|- ( z =/= (/) <-> E. v v e. z ) |
30 |
29
|
anbi2i |
|- ( ( z e. x /\ z =/= (/) ) <-> ( z e. x /\ E. v v e. z ) ) |
31 |
28 30
|
bitr4i |
|- ( E. v ( z e. x /\ v e. z ) <-> ( z e. x /\ z =/= (/) ) ) |
32 |
21 27 31
|
3bitrri |
|- ( ( z e. x /\ z =/= (/) ) <-> z e. dom { <. w , v >. | ( w e. x /\ v e. w ) } ) |
33 |
|
eleq2 |
|- ( dom f = dom { <. w , v >. | ( w e. x /\ v e. w ) } -> ( z e. dom f <-> z e. dom { <. w , v >. | ( w e. x /\ v e. w ) } ) ) |
34 |
32 33
|
bitr4id |
|- ( dom f = dom { <. w , v >. | ( w e. x /\ v e. w ) } -> ( ( z e. x /\ z =/= (/) ) <-> z e. dom f ) ) |
35 |
19 34
|
syl |
|- ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> ( ( z e. x /\ z =/= (/) ) <-> z e. dom f ) ) |
36 |
35
|
adantl |
|- ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( ( z e. x /\ z =/= (/) ) <-> z e. dom f ) ) |
37 |
|
fnfun |
|- ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> Fun f ) |
38 |
|
funfvima3 |
|- ( ( Fun f /\ f C_ { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( z e. dom f -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) ) |
39 |
38
|
ancoms |
|- ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ Fun f ) -> ( z e. dom f -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) ) |
40 |
37 39
|
sylan2 |
|- ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( z e. dom f -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) ) |
41 |
36 40
|
sylbid |
|- ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( ( z e. x /\ z =/= (/) ) -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) ) |
42 |
41
|
imp |
|- ( ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) /\ ( z e. x /\ z =/= (/) ) ) -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) |
43 |
|
imasng |
|- ( z e. _V -> ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u } ) |
44 |
43
|
elv |
|- ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u } |
45 |
|
vex |
|- u e. _V |
46 |
|
elequ1 |
|- ( v = u -> ( v e. z <-> u e. z ) ) |
47 |
46
|
anbi2d |
|- ( v = u -> ( ( z e. x /\ v e. z ) <-> ( z e. x /\ u e. z ) ) ) |
48 |
|
eqid |
|- { <. w , v >. | ( w e. x /\ v e. w ) } = { <. w , v >. | ( w e. x /\ v e. w ) } |
49 |
22 45 25 47 48
|
brab |
|- ( z { <. w , v >. | ( w e. x /\ v e. w ) } u <-> ( z e. x /\ u e. z ) ) |
50 |
49
|
abbii |
|- { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u } = { u | ( z e. x /\ u e. z ) } |
51 |
44 50
|
eqtri |
|- ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | ( z e. x /\ u e. z ) } |
52 |
|
ibar |
|- ( z e. x -> ( u e. z <-> ( z e. x /\ u e. z ) ) ) |
53 |
52
|
abbi2dv |
|- ( z e. x -> z = { u | ( z e. x /\ u e. z ) } ) |
54 |
51 53
|
eqtr4id |
|- ( z e. x -> ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = z ) |
55 |
54
|
eleq2d |
|- ( z e. x -> ( ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) <-> ( f ` z ) e. z ) ) |
56 |
55
|
ad2antrl |
|- ( ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) /\ ( z e. x /\ z =/= (/) ) ) -> ( ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) <-> ( f ` z ) e. z ) ) |
57 |
42 56
|
mpbid |
|- ( ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) /\ ( z e. x /\ z =/= (/) ) ) -> ( f ` z ) e. z ) |
58 |
57
|
exp32 |
|- ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( z e. x -> ( z =/= (/) -> ( f ` z ) e. z ) ) ) |
59 |
58
|
ralrimiv |
|- ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
60 |
59
|
eximi |
|- ( E. f ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
61 |
18 60
|
syl |
|- ( A. y E. f ( f C_ y /\ f Fn dom y ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
62 |
61
|
alrimiv |
|- ( A. y E. f ( f C_ y /\ f Fn dom y ) -> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
63 |
|
eqid |
|- ( w e. dom y |-> ( f ` { u | w y u } ) ) = ( w e. dom y |-> ( f ` { u | w y u } ) ) |
64 |
63
|
aceq3lem |
|- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. f ( f C_ y /\ f Fn dom y ) ) |
65 |
64
|
alrimiv |
|- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. y E. f ( f C_ y /\ f Fn dom y ) ) |
66 |
62 65
|
impbii |
|- ( A. y E. f ( f C_ y /\ f Fn dom y ) <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
67 |
1 66
|
bitri |
|- ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |