Step |
Hyp |
Ref |
Expression |
1 |
|
bnj967.2 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
2 |
|
bnj967.3 |
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) ) |
3 |
|
bnj967.10 |
|- D = ( _om \ { (/) } ) |
4 |
|
bnj967.12 |
|- C = U_ y e. ( f ` m ) _pred ( y , A , R ) |
5 |
|
bnj967.13 |
|- G = ( f u. { <. n , C >. } ) |
6 |
|
bnj967.44 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> C e. _V ) |
7 |
6
|
3adant3 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> C e. _V ) |
8 |
2
|
bnj1235 |
|- ( ch -> f Fn n ) |
9 |
8
|
3ad2ant1 |
|- ( ( ch /\ n = suc m /\ p = suc n ) -> f Fn n ) |
10 |
9
|
3ad2ant2 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> f Fn n ) |
11 |
|
simp23 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> p = suc n ) |
12 |
|
simp3 |
|- ( ( i e. _om /\ suc i e. p /\ suc i e. n ) -> suc i e. n ) |
13 |
12
|
3ad2ant3 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> suc i e. n ) |
14 |
7 10 11 13
|
bnj951 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> ( C e. _V /\ f Fn n /\ p = suc n /\ suc i e. n ) ) |
15 |
3
|
bnj923 |
|- ( n e. D -> n e. _om ) |
16 |
2 15
|
bnj769 |
|- ( ch -> n e. _om ) |
17 |
16
|
3ad2ant1 |
|- ( ( ch /\ n = suc m /\ p = suc n ) -> n e. _om ) |
18 |
17 12
|
bnj240 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> ( n e. _om /\ suc i e. n ) ) |
19 |
|
nnord |
|- ( n e. _om -> Ord n ) |
20 |
|
ordtr |
|- ( Ord n -> Tr n ) |
21 |
19 20
|
syl |
|- ( n e. _om -> Tr n ) |
22 |
|
trsuc |
|- ( ( Tr n /\ suc i e. n ) -> i e. n ) |
23 |
21 22
|
sylan |
|- ( ( n e. _om /\ suc i e. n ) -> i e. n ) |
24 |
18 23
|
syl |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> i e. n ) |
25 |
|
bnj658 |
|- ( ( C e. _V /\ f Fn n /\ p = suc n /\ suc i e. n ) -> ( C e. _V /\ f Fn n /\ p = suc n ) ) |
26 |
25
|
anim1i |
|- ( ( ( C e. _V /\ f Fn n /\ p = suc n /\ suc i e. n ) /\ i e. n ) -> ( ( C e. _V /\ f Fn n /\ p = suc n ) /\ i e. n ) ) |
27 |
|
df-bnj17 |
|- ( ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) <-> ( ( C e. _V /\ f Fn n /\ p = suc n ) /\ i e. n ) ) |
28 |
26 27
|
sylibr |
|- ( ( ( C e. _V /\ f Fn n /\ p = suc n /\ suc i e. n ) /\ i e. n ) -> ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) ) |
29 |
14 24 28
|
syl2anc |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) ) |
30 |
5
|
bnj945 |
|- ( ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) -> ( G ` i ) = ( f ` i ) ) |
31 |
29 30
|
syl |
|- ( ( ( 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 ` i ) = ( f ` i ) ) |
32 |
5
|
bnj945 |
|- ( ( C e. _V /\ f Fn n /\ p = suc n /\ suc i e. n ) -> ( G ` suc i ) = ( f ` suc i ) ) |
33 |
14 32
|
syl |
|- ( ( ( 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 ) = ( f ` suc i ) ) |
34 |
|
3simpb |
|- ( ( i e. _om /\ suc i e. p /\ suc i e. n ) -> ( i e. _om /\ suc i e. n ) ) |
35 |
34
|
3ad2ant3 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> ( i e. _om /\ suc i e. n ) ) |
36 |
2
|
bnj1254 |
|- ( ch -> ps ) |
37 |
36
|
3ad2ant1 |
|- ( ( ch /\ n = suc m /\ p = suc n ) -> ps ) |
38 |
37
|
3ad2ant2 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) -> ps ) |
39 |
31 33 35 38
|
bnj951 |
|- ( ( ( 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 ` i ) = ( f ` i ) /\ ( G ` suc i ) = ( f ` suc i ) /\ ( i e. _om /\ suc i e. n ) /\ ps ) ) |
40 |
4 5
|
bnj958 |
|- ( ( G ` i ) = ( f ` i ) -> A. y ( G ` i ) = ( f ` i ) ) |
41 |
1 40
|
bnj953 |
|- ( ( ( G ` i ) = ( f ` i ) /\ ( G ` suc i ) = ( f ` suc i ) /\ ( i e. _om /\ suc i e. n ) /\ ps ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
42 |
39 41
|
syl |
|- ( ( ( 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 ) ) |