Step |
Hyp |
Ref |
Expression |
1 |
|
bnj910.1 |
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) ) |
2 |
|
bnj910.2 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
3 |
|
bnj910.3 |
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) ) |
4 |
|
bnj910.4 |
|- ( ph' <-> [. p / n ]. ph ) |
5 |
|
bnj910.5 |
|- ( ps' <-> [. p / n ]. ps ) |
6 |
|
bnj910.6 |
|- ( ch' <-> [. p / n ]. ch ) |
7 |
|
bnj910.7 |
|- ( ph" <-> [. G / f ]. ph' ) |
8 |
|
bnj910.8 |
|- ( ps" <-> [. G / f ]. ps' ) |
9 |
|
bnj910.9 |
|- ( ch" <-> [. G / f ]. ch' ) |
10 |
|
bnj910.10 |
|- D = ( _om \ { (/) } ) |
11 |
|
bnj910.11 |
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) } |
12 |
|
bnj910.12 |
|- C = U_ y e. ( f ` m ) _pred ( y , A , R ) |
13 |
|
bnj910.13 |
|- G = ( f u. { <. n , C >. } ) |
14 |
|
bnj910.14 |
|- ( ta <-> ( f Fn n /\ ph /\ ps ) ) |
15 |
|
bnj910.15 |
|- ( si <-> ( n e. D /\ p = suc n /\ m e. n ) ) |
16 |
3 10
|
bnj970 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> p e. D ) |
17 |
1 2 3 10 12 14 15
|
bnj969 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> C e. _V ) |
18 |
|
simpr3 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> p = suc n ) |
19 |
3
|
bnj1235 |
|- ( ch -> f Fn n ) |
20 |
19
|
3ad2ant1 |
|- ( ( ch /\ n = suc m /\ p = suc n ) -> f Fn n ) |
21 |
20
|
adantl |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> f Fn n ) |
22 |
13
|
bnj941 |
|- ( C e. _V -> ( ( p = suc n /\ f Fn n ) -> G Fn p ) ) |
23 |
22
|
3impib |
|- ( ( C e. _V /\ p = suc n /\ f Fn n ) -> G Fn p ) |
24 |
17 18 21 23
|
syl3anc |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> G Fn p ) |
25 |
1 2 3 4 7 10 12 13 14 15
|
bnj944 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) |
26 |
2 3 10 12 13 17
|
bnj967 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
27 |
3 10 12 13 17 24
|
bnj966 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
28 |
2 3 5 8 12 13 26 27
|
bnj964 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) |
29 |
16 24 25 28
|
bnj951 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) |
30 |
|
vex |
|- p e. _V |
31 |
3 4 5 6 30
|
bnj919 |
|- ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) |
32 |
13
|
bnj918 |
|- G e. _V |
33 |
31 7 8 9 32
|
bnj976 |
|- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) |
34 |
29 33
|
sylibr |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) |