Step |
Hyp |
Ref |
Expression |
1 |
|
bnj966.3 |
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) ) |
2 |
|
bnj966.10 |
|- D = ( _om \ { (/) } ) |
3 |
|
bnj966.12 |
|- C = U_ y e. ( f ` m ) _pred ( y , A , R ) |
4 |
|
bnj966.13 |
|- G = ( f u. { <. n , C >. } ) |
5 |
|
bnj966.44 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> C e. _V ) |
6 |
|
bnj966.53 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> G Fn p ) |
7 |
6
|
bnj930 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> Fun G ) |
8 |
7
|
3adant3 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> Fun G ) |
9 |
|
opex |
|- <. n , C >. e. _V |
10 |
9
|
snid |
|- <. n , C >. e. { <. n , C >. } |
11 |
|
elun2 |
|- ( <. n , C >. e. { <. n , C >. } -> <. n , C >. e. ( f u. { <. n , C >. } ) ) |
12 |
10 11
|
ax-mp |
|- <. n , C >. e. ( f u. { <. n , C >. } ) |
13 |
12 4
|
eleqtrri |
|- <. n , C >. e. G |
14 |
|
funopfv |
|- ( Fun G -> ( <. n , C >. e. G -> ( G ` n ) = C ) ) |
15 |
8 13 14
|
mpisyl |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( G ` n ) = C ) |
16 |
|
simp22 |
|- ( ( ( 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 m ) |
17 |
|
simp33 |
|- ( ( ( 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 ) |
18 |
|
bnj551 |
|- ( ( n = suc m /\ n = suc i ) -> m = i ) |
19 |
16 17 18
|
syl2anc |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> m = i ) |
20 |
|
suceq |
|- ( m = i -> suc m = suc i ) |
21 |
20
|
eqeq2d |
|- ( m = i -> ( n = suc m <-> n = suc i ) ) |
22 |
21
|
biimpac |
|- ( ( n = suc m /\ m = i ) -> n = suc i ) |
23 |
22
|
fveq2d |
|- ( ( n = suc m /\ m = i ) -> ( G ` n ) = ( G ` suc i ) ) |
24 |
|
fveq2 |
|- ( m = i -> ( f ` m ) = ( f ` i ) ) |
25 |
24
|
bnj1113 |
|- ( m = i -> U_ y e. ( f ` m ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) |
26 |
3 25
|
syl5eq |
|- ( m = i -> C = U_ y e. ( f ` i ) _pred ( y , A , R ) ) |
27 |
26
|
adantl |
|- ( ( n = suc m /\ m = i ) -> C = U_ y e. ( f ` i ) _pred ( y , A , R ) ) |
28 |
23 27
|
eqeq12d |
|- ( ( n = suc m /\ m = i ) -> ( ( G ` n ) = C <-> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
29 |
16 19 28
|
syl2anc |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( ( G ` n ) = C <-> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
30 |
15 29
|
mpbid |
|- ( ( ( 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. ( f ` i ) _pred ( y , A , R ) ) |
31 |
5
|
3adant3 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> C e. _V ) |
32 |
1
|
bnj1235 |
|- ( ch -> f Fn n ) |
33 |
32
|
3ad2ant1 |
|- ( ( ch /\ n = suc m /\ p = suc n ) -> f Fn n ) |
34 |
33
|
3ad2ant2 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> f Fn n ) |
35 |
|
simp23 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> p = suc n ) |
36 |
31 34 35 17
|
bnj951 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) ) |
37 |
2
|
bnj923 |
|- ( n e. D -> n e. _om ) |
38 |
1 37
|
bnj769 |
|- ( ch -> n e. _om ) |
39 |
38
|
3ad2ant1 |
|- ( ( ch /\ n = suc m /\ p = suc n ) -> n e. _om ) |
40 |
|
simp3 |
|- ( ( i e. _om /\ suc i e. p /\ n = suc i ) -> n = suc i ) |
41 |
39 40
|
bnj240 |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( n e. _om /\ n = suc i ) ) |
42 |
|
vex |
|- i e. _V |
43 |
42
|
bnj216 |
|- ( n = suc i -> i e. n ) |
44 |
43
|
adantl |
|- ( ( n e. _om /\ n = suc i ) -> i e. n ) |
45 |
41 44
|
syl |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> i e. n ) |
46 |
|
bnj658 |
|- ( ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) -> ( C e. _V /\ f Fn n /\ p = suc n ) ) |
47 |
46
|
anim1i |
|- ( ( ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) /\ i e. n ) -> ( ( C e. _V /\ f Fn n /\ p = suc n ) /\ i e. n ) ) |
48 |
|
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 ) ) |
49 |
47 48
|
sylibr |
|- ( ( ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) /\ i e. n ) -> ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) ) |
50 |
4
|
bnj945 |
|- ( ( C e. _V /\ f Fn n /\ p = suc n /\ i e. n ) -> ( G ` i ) = ( f ` i ) ) |
51 |
49 50
|
syl |
|- ( ( ( C e. _V /\ f Fn n /\ p = suc n /\ n = suc i ) /\ i e. n ) -> ( G ` i ) = ( f ` i ) ) |
52 |
36 45 51
|
syl2anc |
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) /\ ( i e. _om /\ suc i e. p /\ n = suc i ) ) -> ( G ` i ) = ( f ` i ) ) |
53 |
3 4
|
bnj958 |
|- ( ( G ` i ) = ( f ` i ) -> A. y ( G ` i ) = ( f ` i ) ) |
54 |
53
|
bnj956 |
|- ( ( G ` i ) = ( f ` i ) -> U_ y e. ( G ` i ) _pred ( y , A , R ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) |
55 |
54
|
eqeq2d |
|- ( ( G ` i ) = ( f ` i ) -> ( ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
56 |
52 55
|
syl |
|- ( ( ( 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 ) <-> ( G ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
57 |
30 56
|
mpbird |
|- ( ( ( 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 ) ) |