Step |
Hyp |
Ref |
Expression |
1 |
|
bnj964.2 |
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
2 |
|
bnj964.3 |
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) ) |
3 |
|
bnj964.5 |
|- ( ps' <-> [. p / n ]. ps ) |
4 |
|
bnj964.8 |
|- ( ps" <-> [. G / f ]. ps' ) |
5 |
|
bnj964.12 |
|- C = U_ y e. ( f ` m ) _pred ( y , A , R ) |
6 |
|
bnj964.13 |
|- G = ( f u. { <. n , C >. } ) |
7 |
|
bnj964.96 |
|- ( ( ( 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 ) ) |
8 |
|
bnj964.165 |
|- ( ( ( 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 ) ) |
9 |
|
nfv |
|- F/ i ( R _FrSe A /\ X e. A ) |
10 |
1
|
bnj1095 |
|- ( ps -> A. i ps ) |
11 |
10 2
|
bnj1096 |
|- ( ch -> A. i ch ) |
12 |
11
|
nf5i |
|- F/ i ch |
13 |
|
nfv |
|- F/ i n = suc m |
14 |
|
nfv |
|- F/ i p = suc n |
15 |
12 13 14
|
nf3an |
|- F/ i ( ch /\ n = suc m /\ p = suc n ) |
16 |
9 15
|
nfan |
|- F/ i ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) |
17 |
|
bnj255 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) <-> ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) |
18 |
|
bnj645 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) -> suc i e. p ) |
19 |
|
simp3 |
|- ( ( ch /\ n = suc m /\ p = suc n ) -> p = suc n ) |
20 |
19
|
bnj706 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) -> p = suc n ) |
21 |
|
eleq2 |
|- ( p = suc n -> ( suc i e. p <-> suc i e. suc n ) ) |
22 |
21
|
biimpac |
|- ( ( suc i e. p /\ p = suc n ) -> suc i e. suc n ) |
23 |
|
elsuci |
|- ( suc i e. suc n -> ( suc i e. n \/ suc i = n ) ) |
24 |
|
eqcom |
|- ( suc i = n <-> n = suc i ) |
25 |
24
|
orbi2i |
|- ( ( suc i e. n \/ suc i = n ) <-> ( suc i e. n \/ n = suc i ) ) |
26 |
23 25
|
sylib |
|- ( suc i e. suc n -> ( suc i e. n \/ n = suc i ) ) |
27 |
22 26
|
syl |
|- ( ( suc i e. p /\ p = suc n ) -> ( suc i e. n \/ n = suc i ) ) |
28 |
18 20 27
|
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 \/ n = suc i ) ) |
29 |
|
df-3an |
|- ( ( i e. _om /\ suc i e. p /\ suc i e. n ) <-> ( ( i e. _om /\ suc i e. p ) /\ suc i e. n ) ) |
30 |
29
|
3anbi3i |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) <-> ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( ( i e. _om /\ suc i e. p ) /\ suc i e. n ) ) ) |
31 |
|
bnj255 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) /\ suc i e. n ) <-> ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( ( i e. _om /\ suc i e. p ) /\ suc i e. n ) ) ) |
32 |
30 31
|
bitr4i |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ suc i e. n ) ) <-> ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) /\ suc i e. n ) ) |
33 |
|
bnj345 |
|- ( ( ( 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 /\ ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) |
34 |
|
bnj252 |
|- ( ( suc i e. n /\ ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) <-> ( suc i e. n /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) ) |
35 |
32 33 34
|
3bitri |
|- ( ( ( 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 /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) ) |
36 |
17
|
anbi2i |
|- ( ( suc i e. n /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) ) <-> ( suc i e. n /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) ) |
37 |
35 36
|
bitr4i |
|- ( ( ( 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 /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) ) ) |
38 |
37 7
|
sylbir |
|- ( ( suc i e. n /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
39 |
38
|
ex |
|- ( suc i e. n -> ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
40 |
|
df-3an |
|- ( ( i e. _om /\ suc i e. p /\ n = suc i ) <-> ( ( i e. _om /\ suc i e. p ) /\ n = suc i ) ) |
41 |
40
|
3anbi3i |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) <-> ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( ( i e. _om /\ suc i e. p ) /\ n = suc i ) ) ) |
42 |
|
bnj255 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) /\ n = suc i ) <-> ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( ( i e. _om /\ suc i e. p ) /\ n = suc i ) ) ) |
43 |
41 42
|
bitr4i |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) <-> ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) /\ n = suc i ) ) |
44 |
|
bnj345 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) /\ n = suc i ) <-> ( n = suc i /\ ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) |
45 |
|
bnj252 |
|- ( ( n = suc i /\ ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) <-> ( n = suc i /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) ) |
46 |
43 44 45
|
3bitri |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) <-> ( n = suc i /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) ) |
47 |
17
|
anbi2i |
|- ( ( n = suc i /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) ) <-> ( n = suc i /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) ) ) |
48 |
46 47
|
bitr4i |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) <-> ( n = suc i /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) ) ) |
49 |
48 8
|
sylbir |
|- ( ( n = suc i /\ ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
50 |
49
|
ex |
|- ( n = suc i -> ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
51 |
39 50
|
jaoi |
|- ( ( suc i e. n \/ n = suc i ) -> ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
52 |
28 51
|
mpcom |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
53 |
17 52
|
sylbir |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
54 |
53
|
3expia |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( ( i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
55 |
16 54
|
alrimi |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> A. i ( ( i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
56 |
|
vex |
|- p e. _V |
57 |
1 3 56
|
bnj539 |
|- ( ps' <-> A. i e. _om ( suc i e. p -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
58 |
57 4 5 6
|
bnj965 |
|- ( ps" <-> A. i e. _om ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
59 |
58
|
bnj115 |
|- ( ps" <-> A. i ( ( i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
60 |
55 59
|
sylibr |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) |