Metamath Proof Explorer


Theorem bnj964

Description: Technical lemma for bnj69 . 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 bnj964.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj964.3 χ n D f Fn n φ ψ
bnj964.5 No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
bnj964.8 No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
bnj964.12 C = y f m pred y A R
bnj964.13 G = f n C
bnj964.96 R FrSe A X A χ n = suc m p = suc n i ω suc i p suc i n G suc i = y G i pred y A R
bnj964.165 R FrSe A X A χ n = suc m p = suc n i ω suc i p n = suc i G suc i = y G i pred y A R
Assertion bnj964 Could not format assertion : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ps" ) with typecode |-

Proof

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