Step |
Hyp |
Ref |
Expression |
1 |
|
bnj151.1 |
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) ) |
2 |
|
bnj151.2 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
3 |
|
bnj151.3 |
|- D = ( _om \ { (/) } ) |
4 |
|
bnj151.4 |
|- ( th <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn n /\ ph /\ ps ) ) ) |
5 |
|
bnj151.5 |
|- ( ta <-> A. m e. D ( m _E n -> [. m / n ]. th ) ) |
6 |
|
bnj151.6 |
|- ( ze <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) ) |
7 |
|
bnj151.7 |
|- ( ph' <-> [. 1o / n ]. ph ) |
8 |
|
bnj151.8 |
|- ( ps' <-> [. 1o / n ]. ps ) |
9 |
|
bnj151.9 |
|- ( th' <-> [. 1o / n ]. th ) |
10 |
|
bnj151.10 |
|- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) |
11 |
|
bnj151.11 |
|- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) |
12 |
|
bnj151.12 |
|- ( ze' <-> [. 1o / n ]. ze ) |
13 |
|
bnj151.13 |
|- F = { <. (/) , _pred ( x , A , R ) >. } |
14 |
|
bnj151.14 |
|- ( ph" <-> [. F / f ]. ph' ) |
15 |
|
bnj151.15 |
|- ( ps" <-> [. F / f ]. ps' ) |
16 |
|
bnj151.16 |
|- ( ze" <-> [. F / f ]. ze' ) |
17 |
|
bnj151.17 |
|- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) |
18 |
|
bnj151.18 |
|- ( ze1 <-> [. g / f ]. ze0 ) |
19 |
|
bnj151.19 |
|- ( ph1 <-> [. g / f ]. ph' ) |
20 |
|
bnj151.20 |
|- ( ps1 <-> [. g / f ]. ps' ) |
21 |
1 2 6 7 8 10 12 13 14 15 16
|
bnj150 |
|- th0 |
22 |
21 10
|
mpbi |
|- ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) |
23 |
1 7
|
bnj118 |
|- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) |
24 |
11 17 18 19 20 23
|
bnj149 |
|- th1 |
25 |
24 11
|
mpbi |
|- ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) |
26 |
|
df-eu |
|- ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> ( E. f ( f Fn 1o /\ ph' /\ ps' ) /\ E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) |
27 |
22 25 26
|
sylanbrc |
|- ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) |
28 |
4 7 8 9
|
bnj130 |
|- ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) ) |
29 |
27 28
|
mpbir |
|- th' |
30 |
|
sbceq1a |
|- ( n = 1o -> ( th <-> [. 1o / n ]. th ) ) |
31 |
30 9
|
bitr4di |
|- ( n = 1o -> ( th <-> th' ) ) |
32 |
29 31
|
mpbiri |
|- ( n = 1o -> th ) |
33 |
32
|
a1d |
|- ( n = 1o -> ( ( n e. D /\ ta ) -> th ) ) |