Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
|- x e. _V |
2 |
|
omex |
|- _om e. _V |
3 |
|
isacn |
|- ( ( x e. _V /\ _om e. _V ) -> ( x e. AC_ _om <-> A. f e. ( ( ~P x \ { (/) } ) ^m _om ) E. g A. y e. _om ( g ` y ) e. ( f ` y ) ) ) |
4 |
1 2 3
|
mp2an |
|- ( x e. AC_ _om <-> A. f e. ( ( ~P x \ { (/) } ) ^m _om ) E. g A. y e. _om ( g ` y ) e. ( f ` y ) ) |
5 |
|
axcc2 |
|- E. g ( g Fn _om /\ A. y e. _om ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) ) |
6 |
|
elmapi |
|- ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> f : _om --> ( ~P x \ { (/) } ) ) |
7 |
|
ffvelrn |
|- ( ( f : _om --> ( ~P x \ { (/) } ) /\ y e. _om ) -> ( f ` y ) e. ( ~P x \ { (/) } ) ) |
8 |
|
eldifsni |
|- ( ( f ` y ) e. ( ~P x \ { (/) } ) -> ( f ` y ) =/= (/) ) |
9 |
7 8
|
syl |
|- ( ( f : _om --> ( ~P x \ { (/) } ) /\ y e. _om ) -> ( f ` y ) =/= (/) ) |
10 |
6 9
|
sylan |
|- ( ( f e. ( ( ~P x \ { (/) } ) ^m _om ) /\ y e. _om ) -> ( f ` y ) =/= (/) ) |
11 |
|
id |
|- ( ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) -> ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) ) |
12 |
10 11
|
syl5com |
|- ( ( f e. ( ( ~P x \ { (/) } ) ^m _om ) /\ y e. _om ) -> ( ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) -> ( g ` y ) e. ( f ` y ) ) ) |
13 |
12
|
ralimdva |
|- ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> ( A. y e. _om ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) -> A. y e. _om ( g ` y ) e. ( f ` y ) ) ) |
14 |
13
|
adantld |
|- ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> ( ( g Fn _om /\ A. y e. _om ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) ) -> A. y e. _om ( g ` y ) e. ( f ` y ) ) ) |
15 |
14
|
eximdv |
|- ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> ( E. g ( g Fn _om /\ A. y e. _om ( ( f ` y ) =/= (/) -> ( g ` y ) e. ( f ` y ) ) ) -> E. g A. y e. _om ( g ` y ) e. ( f ` y ) ) ) |
16 |
5 15
|
mpi |
|- ( f e. ( ( ~P x \ { (/) } ) ^m _om ) -> E. g A. y e. _om ( g ` y ) e. ( f ` y ) ) |
17 |
4 16
|
mprgbir |
|- x e. AC_ _om |
18 |
17 1
|
2th |
|- ( x e. AC_ _om <-> x e. _V ) |
19 |
18
|
eqriv |
|- AC_ _om = _V |