Step |
Hyp |
Ref |
Expression |
1 |
|
bnj852.1 |
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) ) |
2 |
|
bnj852.2 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
3 |
|
bnj852.3 |
|- D = ( _om \ { (/) } ) |
4 |
|
elisset |
|- ( X e. A -> E. x x = X ) |
5 |
4
|
adantl |
|- ( ( R _FrSe A /\ X e. A ) -> E. x x = X ) |
6 |
5
|
ancri |
|- ( ( R _FrSe A /\ X e. A ) -> ( E. x x = X /\ ( R _FrSe A /\ X e. A ) ) ) |
7 |
6
|
bnj534 |
|- ( ( R _FrSe A /\ X e. A ) -> E. x ( x = X /\ ( R _FrSe A /\ X e. A ) ) ) |
8 |
|
eleq1 |
|- ( x = X -> ( x e. A <-> X e. A ) ) |
9 |
8
|
anbi2d |
|- ( x = X -> ( ( R _FrSe A /\ x e. A ) <-> ( R _FrSe A /\ X e. A ) ) ) |
10 |
9
|
biimpar |
|- ( ( x = X /\ ( R _FrSe A /\ X e. A ) ) -> ( R _FrSe A /\ x e. A ) ) |
11 |
|
biid |
|- ( A. z e. D ( z _E n -> [. z / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) <-> A. z e. D ( z _E n -> [. z / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) ) |
12 |
|
omex |
|- _om e. _V |
13 |
|
difexg |
|- ( _om e. _V -> ( _om \ { (/) } ) e. _V ) |
14 |
12 13
|
ax-mp |
|- ( _om \ { (/) } ) e. _V |
15 |
3 14
|
eqeltri |
|- D e. _V |
16 |
|
zfregfr |
|- _E Fr D |
17 |
11 15 16
|
bnj157 |
|- ( A. n e. D ( A. z e. D ( z _E n -> [. z / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) -> A. n e. D ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) |
18 |
|
biid |
|- ( ( f ` (/) ) = _pred ( x , A , R ) <-> ( f ` (/) ) = _pred ( x , A , R ) ) |
19 |
|
biid |
|- ( ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) |
20 |
18 2 3 19 11
|
bnj153 |
|- ( n = 1o -> ( ( n e. D /\ A. z e. D ( z _E n -> [. z / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) ) -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) ) |
21 |
18 2 3 19 11
|
bnj601 |
|- ( n =/= 1o -> ( ( n e. D /\ A. z e. D ( z _E n -> [. z / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) ) -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) ) |
22 |
20 21
|
pm2.61ine |
|- ( ( n e. D /\ A. z e. D ( z _E n -> [. z / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) ) -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) |
23 |
22
|
ex |
|- ( n e. D -> ( A. z e. D ( z _E n -> [. z / n ]. ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) ) |
24 |
17 23
|
mprg |
|- A. n e. D ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) |
25 |
|
r19.21v |
|- ( A. n e. D ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) <-> ( ( R _FrSe A /\ x e. A ) -> A. n e. D E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) ) |
26 |
24 25
|
mpbi |
|- ( ( R _FrSe A /\ x e. A ) -> A. n e. D E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) |
27 |
10 26
|
syl |
|- ( ( x = X /\ ( R _FrSe A /\ X e. A ) ) -> A. n e. D E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) ) |
28 |
|
bnj602 |
|- ( x = X -> _pred ( x , A , R ) = _pred ( X , A , R ) ) |
29 |
28
|
eqeq2d |
|- ( x = X -> ( ( f ` (/) ) = _pred ( x , A , R ) <-> ( f ` (/) ) = _pred ( X , A , R ) ) ) |
30 |
29 1
|
bitr4di |
|- ( x = X -> ( ( f ` (/) ) = _pred ( x , A , R ) <-> ph ) ) |
31 |
30
|
3anbi2d |
|- ( x = X -> ( ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) <-> ( f Fn n /\ ph /\ ps ) ) ) |
32 |
31
|
eubidv |
|- ( x = X -> ( E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) <-> E! f ( f Fn n /\ ph /\ ps ) ) ) |
33 |
32
|
ralbidv |
|- ( x = X -> ( A. n e. D E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) <-> A. n e. D E! f ( f Fn n /\ ph /\ ps ) ) ) |
34 |
33
|
adantr |
|- ( ( x = X /\ ( R _FrSe A /\ X e. A ) ) -> ( A. n e. D E! f ( f Fn n /\ ( f ` (/) ) = _pred ( x , A , R ) /\ ps ) <-> A. n e. D E! f ( f Fn n /\ ph /\ ps ) ) ) |
35 |
27 34
|
mpbid |
|- ( ( x = X /\ ( R _FrSe A /\ X e. A ) ) -> A. n e. D E! f ( f Fn n /\ ph /\ ps ) ) |
36 |
7 35
|
bnj593 |
|- ( ( R _FrSe A /\ X e. A ) -> E. x A. n e. D E! f ( f Fn n /\ ph /\ ps ) ) |
37 |
36
|
bnj937 |
|- ( ( R _FrSe A /\ X e. A ) -> A. n e. D E! f ( f Fn n /\ ph /\ ps ) ) |