Metamath Proof Explorer


Theorem bnj910

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 bnj910.1 φ f = pred X A R
bnj910.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj910.3 χ n D f Fn n φ ψ
bnj910.4 No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
bnj910.5 No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
bnj910.6 No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
bnj910.7 No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
bnj910.8 No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
bnj910.9 No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
bnj910.10 D = ω
bnj910.11 B = f | n D f Fn n φ ψ
bnj910.12 C = y f m pred y A R
bnj910.13 G = f n C
bnj910.14 τ f Fn n φ ψ
bnj910.15 σ n D p = suc n m n
Assertion bnj910 Could not format assertion : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj910.1 φ f = pred X A R
2 bnj910.2 ψ i ω suc i n f suc i = y f i pred y A R
3 bnj910.3 χ n D f Fn n φ ψ
4 bnj910.4 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
5 bnj910.5 Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
6 bnj910.6 Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
7 bnj910.7 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
8 bnj910.8 Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
9 bnj910.9 Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
10 bnj910.10 D = ω
11 bnj910.11 B = f | n D f Fn n φ ψ
12 bnj910.12 C = y f m pred y A R
13 bnj910.13 G = f n C
14 bnj910.14 τ f Fn n φ ψ
15 bnj910.15 σ n D p = suc n m n
16 3 10 bnj970 R FrSe A X A χ n = suc m p = suc n p D
17 1 2 3 10 12 14 15 bnj969 R FrSe A X A χ n = suc m p = suc n C V
18 simpr3 R FrSe A X A χ n = suc m p = suc n p = suc n
19 3 bnj1235 χ f Fn n
20 19 3ad2ant1 χ n = suc m p = suc n f Fn n
21 20 adantl R FrSe A X A χ n = suc m p = suc n f Fn n
22 13 bnj941 C V p = suc n f Fn n G Fn p
23 22 3impib C V p = suc n f Fn n G Fn p
24 17 18 21 23 syl3anc R FrSe A X A χ n = suc m p = suc n G Fn p
25 1 2 3 4 7 10 12 13 14 15 bnj944 Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) with typecode |-
26 2 3 10 12 13 17 bnj967 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
27 3 10 12 13 17 24 bnj966 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
28 2 3 5 8 12 13 26 27 bnj964 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 |-
29 16 24 25 28 bnj951 Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |-
30 vex p V
31 3 4 5 6 30 bnj919 Could not format ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) with typecode |-
32 13 bnj918 G V
33 31 7 8 9 32 bnj976 Could not format ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for |- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |-
34 29 33 sylibr Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ch" ) with typecode |-