Step |
Hyp |
Ref |
Expression |
1 |
|
axcc4dom.1 |
|- A e. _V |
2 |
|
axcc4dom.2 |
|- ( x = ( f ` n ) -> ( ph <-> ps ) ) |
3 |
|
brdom2 |
|- ( N ~<_ _om <-> ( N ~< _om \/ N ~~ _om ) ) |
4 |
|
isfinite |
|- ( N e. Fin <-> N ~< _om ) |
5 |
2
|
ac6sfi |
|- ( ( N e. Fin /\ A. n e. N E. x e. A ph ) -> E. f ( f : N --> A /\ A. n e. N ps ) ) |
6 |
5
|
ex |
|- ( N e. Fin -> ( A. n e. N E. x e. A ph -> E. f ( f : N --> A /\ A. n e. N ps ) ) ) |
7 |
4 6
|
sylbir |
|- ( N ~< _om -> ( A. n e. N E. x e. A ph -> E. f ( f : N --> A /\ A. n e. N ps ) ) ) |
8 |
|
raleq |
|- ( N = if ( N ~~ _om , N , _om ) -> ( A. n e. N E. x e. A ph <-> A. n e. if ( N ~~ _om , N , _om ) E. x e. A ph ) ) |
9 |
|
feq2 |
|- ( N = if ( N ~~ _om , N , _om ) -> ( f : N --> A <-> f : if ( N ~~ _om , N , _om ) --> A ) ) |
10 |
|
raleq |
|- ( N = if ( N ~~ _om , N , _om ) -> ( A. n e. N ps <-> A. n e. if ( N ~~ _om , N , _om ) ps ) ) |
11 |
9 10
|
anbi12d |
|- ( N = if ( N ~~ _om , N , _om ) -> ( ( f : N --> A /\ A. n e. N ps ) <-> ( f : if ( N ~~ _om , N , _om ) --> A /\ A. n e. if ( N ~~ _om , N , _om ) ps ) ) ) |
12 |
11
|
exbidv |
|- ( N = if ( N ~~ _om , N , _om ) -> ( E. f ( f : N --> A /\ A. n e. N ps ) <-> E. f ( f : if ( N ~~ _om , N , _om ) --> A /\ A. n e. if ( N ~~ _om , N , _om ) ps ) ) ) |
13 |
8 12
|
imbi12d |
|- ( N = if ( N ~~ _om , N , _om ) -> ( ( A. n e. N E. x e. A ph -> E. f ( f : N --> A /\ A. n e. N ps ) ) <-> ( A. n e. if ( N ~~ _om , N , _om ) E. x e. A ph -> E. f ( f : if ( N ~~ _om , N , _om ) --> A /\ A. n e. if ( N ~~ _om , N , _om ) ps ) ) ) ) |
14 |
|
breq1 |
|- ( N = if ( N ~~ _om , N , _om ) -> ( N ~~ _om <-> if ( N ~~ _om , N , _om ) ~~ _om ) ) |
15 |
|
breq1 |
|- ( _om = if ( N ~~ _om , N , _om ) -> ( _om ~~ _om <-> if ( N ~~ _om , N , _om ) ~~ _om ) ) |
16 |
|
omex |
|- _om e. _V |
17 |
16
|
enref |
|- _om ~~ _om |
18 |
14 15 17
|
elimhyp |
|- if ( N ~~ _om , N , _om ) ~~ _om |
19 |
1 18 2
|
axcc4 |
|- ( A. n e. if ( N ~~ _om , N , _om ) E. x e. A ph -> E. f ( f : if ( N ~~ _om , N , _om ) --> A /\ A. n e. if ( N ~~ _om , N , _om ) ps ) ) |
20 |
13 19
|
dedth |
|- ( N ~~ _om -> ( A. n e. N E. x e. A ph -> E. f ( f : N --> A /\ A. n e. N ps ) ) ) |
21 |
7 20
|
jaoi |
|- ( ( N ~< _om \/ N ~~ _om ) -> ( A. n e. N E. x e. A ph -> E. f ( f : N --> A /\ A. n e. N ps ) ) ) |
22 |
3 21
|
sylbi |
|- ( N ~<_ _om -> ( A. n e. N E. x e. A ph -> E. f ( f : N --> A /\ A. n e. N ps ) ) ) |
23 |
22
|
imp |
|- ( ( N ~<_ _om /\ A. n e. N E. x e. A ph ) -> E. f ( f : N --> A /\ A. n e. N ps ) ) |