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