Metamath Proof Explorer


Theorem bnj1000

Description: Technical lemma for bnj852 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1000.1 ψ i ω suc i N f suc i = y f i pred y A R
bnj1000.2 No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
bnj1000.3 G V
bnj1000.15 C = y f m pred y A R
bnj1000.16 G = f n C
Assertion bnj1000 Could not format assertion : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj1000.1 ψ i ω suc i N f suc i = y f i pred y A R
2 bnj1000.2 Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
3 bnj1000.3 G V
4 bnj1000.15 C = y f m pred y A R
5 bnj1000.16 G = f n C
6 df-ral i ω suc i N f suc i = y f i pred y A R i i ω suc i N f suc i = y f i pred y A R
7 6 bicomi i i ω suc i N f suc i = y f i pred y A R i ω suc i N f suc i = y f i pred y A R
8 7 sbcbii [˙G / f]˙ i i ω suc i N f suc i = y f i pred y A R [˙G / f]˙ i ω suc i N f suc i = y f i pred y A R
9 nfv f i ω
10 9 sbc19.21g G V [˙G / f]˙ i ω suc i N f suc i = y f i pred y A R i ω [˙G / f]˙ suc i N f suc i = y f i pred y A R
11 3 10 ax-mp [˙G / f]˙ i ω suc i N f suc i = y f i pred y A R i ω [˙G / f]˙ suc i N f suc i = y f i pred y A R
12 nfv f suc i N
13 12 sbc19.21g G V [˙G / f]˙ suc i N f suc i = y f i pred y A R suc i N [˙G / f]˙ f suc i = y f i pred y A R
14 3 13 ax-mp [˙G / f]˙ suc i N f suc i = y f i pred y A R suc i N [˙G / f]˙ f suc i = y f i pred y A R
15 fveq1 f = G f suc i = G suc i
16 fveq1 f = G f i = G i
17 ax-5 w f i y w f i
18 nfcv _ y f
19 nfcv _ y n
20 nfiu1 _ y y f m pred y A R
21 4 20 nfcxfr _ y C
22 19 21 nfop _ y n C
23 22 nfsn _ y n C
24 18 23 nfun _ y f n C
25 5 24 nfcxfr _ y G
26 nfcv _ y i
27 25 26 nffv _ y G i
28 27 nfcrii w G i y w G i
29 17 28 bnj1316 f i = G i y f i pred y A R = y G i pred y A R
30 16 29 syl f = G y f i pred y A R = y G i pred y A R
31 15 30 eqeq12d f = G f suc i = y f i pred y A R G suc i = y G i pred y A R
32 fveq1 f = e f suc i = e suc i
33 fveq1 f = e f i = e i
34 ax-5 f i = e i y f i = e i
35 34 bnj956 f i = e i y f i pred y A R = y e i pred y A R
36 33 35 syl f = e y f i pred y A R = y e i pred y A R
37 32 36 eqeq12d f = e f suc i = y f i pred y A R e suc i = y e i pred y A R
38 fveq1 e = G e suc i = G suc i
39 fveq1 e = G e i = G i
40 ax-5 w e i y w e i
41 40 28 bnj1316 e i = G i y e i pred y A R = y G i pred y A R
42 39 41 syl e = G y e i pred y A R = y G i pred y A R
43 38 42 eqeq12d e = G e suc i = y e i pred y A R G suc i = y G i pred y A R
44 3 31 37 43 bnj610 [˙G / f]˙ f suc i = y f i pred y A R G suc i = y G i pred y A R
45 44 imbi2i suc i N [˙G / f]˙ f suc i = y f i pred y A R suc i N G suc i = y G i pred y A R
46 14 45 bitri [˙G / f]˙ suc i N f suc i = y f i pred y A R suc i N G suc i = y G i pred y A R
47 46 imbi2i i ω [˙G / f]˙ suc i N f suc i = y f i pred y A R i ω suc i N G suc i = y G i pred y A R
48 11 47 bitri [˙G / f]˙ i ω suc i N f suc i = y f i pred y A R i ω suc i N G suc i = y G i pred y A R
49 48 albii i [˙G / f]˙ i ω suc i N f suc i = y f i pred y A R i i ω suc i N G suc i = y G i pred y A R
50 sbcal [˙G / f]˙ i i ω suc i N f suc i = y f i pred y A R i [˙G / f]˙ i ω suc i N f suc i = y f i pred y A R
51 df-ral i ω suc i N G suc i = y G i pred y A R i i ω suc i N G suc i = y G i pred y A R
52 49 50 51 3bitr4ri i ω suc i N G suc i = y G i pred y A R [˙G / f]˙ i i ω suc i N f suc i = y f i pred y A R
53 1 sbcbii [˙G / f]˙ ψ [˙G / f]˙ i ω suc i N f suc i = y f i pred y A R
54 8 52 53 3bitr4ri [˙G / f]˙ ψ i ω suc i N G suc i = y G i pred y A R
55 2 54 bitri Could not format ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode |-