Step |
Hyp |
Ref |
Expression |
1 |
|
uniexr |
|- ( U. A e. dom card -> A e. _V ) |
2 |
|
dfac8b |
|- ( U. A e. dom card -> E. r r We U. A ) |
3 |
|
dfac8c |
|- ( A e. _V -> ( E. r r We U. A -> E. g A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) ) |
4 |
1 2 3
|
sylc |
|- ( U. A e. dom card -> E. g A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) |
5 |
4
|
adantr |
|- ( ( U. A e. dom card /\ -. (/) e. A ) -> E. g A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) |
6 |
1
|
ad2antrr |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> A e. _V ) |
7 |
6
|
mptexd |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> ( y e. A |-> ( g ` y ) ) e. _V ) |
8 |
|
nelne2 |
|- ( ( x e. A /\ -. (/) e. A ) -> x =/= (/) ) |
9 |
8
|
ancoms |
|- ( ( -. (/) e. A /\ x e. A ) -> x =/= (/) ) |
10 |
9
|
adantll |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ x e. A ) -> x =/= (/) ) |
11 |
|
pm2.27 |
|- ( x =/= (/) -> ( ( x =/= (/) -> ( g ` x ) e. x ) -> ( g ` x ) e. x ) ) |
12 |
10 11
|
syl |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ x e. A ) -> ( ( x =/= (/) -> ( g ` x ) e. x ) -> ( g ` x ) e. x ) ) |
13 |
12
|
ralimdva |
|- ( ( U. A e. dom card /\ -. (/) e. A ) -> ( A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) -> A. x e. A ( g ` x ) e. x ) ) |
14 |
13
|
imp |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> A. x e. A ( g ` x ) e. x ) |
15 |
|
fveq2 |
|- ( x = y -> ( g ` x ) = ( g ` y ) ) |
16 |
|
id |
|- ( x = y -> x = y ) |
17 |
15 16
|
eleq12d |
|- ( x = y -> ( ( g ` x ) e. x <-> ( g ` y ) e. y ) ) |
18 |
17
|
rspccva |
|- ( ( A. x e. A ( g ` x ) e. x /\ y e. A ) -> ( g ` y ) e. y ) |
19 |
14 18
|
sylan |
|- ( ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) /\ y e. A ) -> ( g ` y ) e. y ) |
20 |
|
elunii |
|- ( ( ( g ` y ) e. y /\ y e. A ) -> ( g ` y ) e. U. A ) |
21 |
19 20
|
sylancom |
|- ( ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) /\ y e. A ) -> ( g ` y ) e. U. A ) |
22 |
21
|
fmpttd |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> ( y e. A |-> ( g ` y ) ) : A --> U. A ) |
23 |
|
fveq2 |
|- ( y = x -> ( g ` y ) = ( g ` x ) ) |
24 |
|
eqid |
|- ( y e. A |-> ( g ` y ) ) = ( y e. A |-> ( g ` y ) ) |
25 |
|
fvex |
|- ( g ` x ) e. _V |
26 |
23 24 25
|
fvmpt |
|- ( x e. A -> ( ( y e. A |-> ( g ` y ) ) ` x ) = ( g ` x ) ) |
27 |
26
|
eleq1d |
|- ( x e. A -> ( ( ( y e. A |-> ( g ` y ) ) ` x ) e. x <-> ( g ` x ) e. x ) ) |
28 |
27
|
ralbiia |
|- ( A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x <-> A. x e. A ( g ` x ) e. x ) |
29 |
14 28
|
sylibr |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) |
30 |
22 29
|
jca |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> ( ( y e. A |-> ( g ` y ) ) : A --> U. A /\ A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) ) |
31 |
|
feq1 |
|- ( f = ( y e. A |-> ( g ` y ) ) -> ( f : A --> U. A <-> ( y e. A |-> ( g ` y ) ) : A --> U. A ) ) |
32 |
|
fveq1 |
|- ( f = ( y e. A |-> ( g ` y ) ) -> ( f ` x ) = ( ( y e. A |-> ( g ` y ) ) ` x ) ) |
33 |
32
|
eleq1d |
|- ( f = ( y e. A |-> ( g ` y ) ) -> ( ( f ` x ) e. x <-> ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) ) |
34 |
33
|
ralbidv |
|- ( f = ( y e. A |-> ( g ` y ) ) -> ( A. x e. A ( f ` x ) e. x <-> A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) ) |
35 |
31 34
|
anbi12d |
|- ( f = ( y e. A |-> ( g ` y ) ) -> ( ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) <-> ( ( y e. A |-> ( g ` y ) ) : A --> U. A /\ A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) ) ) |
36 |
7 30 35
|
spcedv |
|- ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> E. f ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) ) |
37 |
5 36
|
exlimddv |
|- ( ( U. A e. dom card /\ -. (/) e. A ) -> E. f ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) ) |