Step |
Hyp |
Ref |
Expression |
1 |
|
bnj611.1 |
|- ( ps <-> A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
2 |
|
bnj611.2 |
|- ( ps" <-> [. G / f ]. ps ) |
3 |
|
bnj611.3 |
|- G e. _V |
4 |
|
df-ral |
|- ( A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) |
5 |
4
|
bicomi |
|- ( A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
6 |
5
|
sbcbii |
|- ( [. G / f ]. A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> [. G / f ]. A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
7 |
|
nfv |
|- F/ f i e. _om |
8 |
7
|
sbc19.21g |
|- ( G e. _V -> ( [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( i e. _om -> [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) ) |
9 |
3 8
|
ax-mp |
|- ( [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( i e. _om -> [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) |
10 |
|
nfv |
|- F/ f suc i e. N |
11 |
10
|
sbc19.21g |
|- ( G e. _V -> ( [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) |
12 |
3 11
|
ax-mp |
|- ( [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
13 |
|
fveq1 |
|- ( f = G -> ( f ` suc i ) = ( G ` suc i ) ) |
14 |
|
fveq1 |
|- ( f = G -> ( f ` i ) = ( G ` i ) ) |
15 |
14
|
bnj1113 |
|- ( f = G -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
16 |
13 15
|
eqeq12d |
|- ( f = G -> ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
17 |
|
fveq1 |
|- ( f = e -> ( f ` suc i ) = ( e ` suc i ) ) |
18 |
|
fveq1 |
|- ( f = e -> ( f ` i ) = ( e ` i ) ) |
19 |
18
|
bnj1113 |
|- ( f = e -> U_ y e. ( f ` i ) _pred ( y , A , R ) = U_ y e. ( e ` i ) _pred ( y , A , R ) ) |
20 |
17 19
|
eqeq12d |
|- ( f = e -> ( ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( e ` suc i ) = U_ y e. ( e ` i ) _pred ( y , A , R ) ) ) |
21 |
|
fveq1 |
|- ( e = G -> ( e ` suc i ) = ( G ` suc i ) ) |
22 |
|
fveq1 |
|- ( e = G -> ( e ` i ) = ( G ` i ) ) |
23 |
22
|
bnj1113 |
|- ( e = G -> U_ y e. ( e ` i ) _pred ( y , A , R ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
24 |
21 23
|
eqeq12d |
|- ( e = G -> ( ( e ` suc i ) = U_ y e. ( e ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
25 |
3 16 20 24
|
bnj610 |
|- ( [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) <-> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) |
26 |
25
|
imbi2i |
|- ( ( suc i e. N -> [. G / f ]. ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
27 |
12 26
|
bitri |
|- ( [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) <-> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
28 |
27
|
imbi2i |
|- ( ( i e. _om -> [. G / f ]. ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( i e. _om -> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) ) |
29 |
9 28
|
bitri |
|- ( [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> ( i e. _om -> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) ) |
30 |
29
|
albii |
|- ( A. i [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> A. i ( i e. _om -> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) ) |
31 |
|
sbcal |
|- ( [. G / f ]. A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) <-> A. i [. G / f ]. ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) |
32 |
|
df-ral |
|- ( A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) <-> A. i ( i e. _om -> ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) ) |
33 |
30 31 32
|
3bitr4ri |
|- ( A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) <-> [. G / f ]. A. i ( i e. _om -> ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) |
34 |
1
|
sbcbii |
|- ( [. G / f ]. ps <-> [. G / f ]. A. i e. _om ( suc i e. N -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) |
35 |
6 33 34
|
3bitr4ri |
|- ( [. G / f ]. ps <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |
36 |
2 35
|
bitri |
|- ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) |