Metamath Proof Explorer


Theorem bnj970

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 bnj970.3 χ n D f Fn n φ ψ
bnj970.10 D = ω
Assertion bnj970 R FrSe A X A χ n = suc m p = suc n p D

Proof

Step Hyp Ref Expression
1 bnj970.3 χ n D f Fn n φ ψ
2 bnj970.10 D = ω
3 1 bnj1232 χ n D
4 3 3ad2ant1 χ n = suc m p = suc n n D
5 4 adantl R FrSe A X A χ n = suc m p = suc n n D
6 simpr3 R FrSe A X A χ n = suc m p = suc n p = suc n
7 2 bnj923 n D n ω
8 peano2 n ω suc n ω
9 eleq1 p = suc n p ω suc n ω
10 bianir suc n ω p ω suc n ω p ω
11 8 9 10 syl2an n ω p = suc n p ω
12 7 11 sylan n D p = suc n p ω
13 df-suc suc n = n n
14 13 eqeq2i p = suc n p = n n
15 ssun2 n n n
16 vex n V
17 16 snnz n
18 ssn0 n n n n n n
19 15 17 18 mp2an n n
20 neeq1 p = n n p n n
21 19 20 mpbiri p = n n p
22 14 21 sylbi p = suc n p
23 22 adantl n D p = suc n p
24 2 eleq2i p D p ω
25 eldifsn p ω p ω p
26 24 25 bitri p D p ω p
27 12 23 26 sylanbrc n D p = suc n p D
28 5 6 27 syl2anc R FrSe A X A χ n = suc m p = suc n p D