bnj1001

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	bnj1001.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj1001.5	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
	bnj1001.6	⊢ ( 𝜂 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
	bnj1001.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj1001.27	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝜒″ )
Assertion	bnj1001	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1001.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
2		bnj1001.5	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
3		bnj1001.6	⊢ ( 𝜂 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
4		bnj1001.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
5		bnj1001.27	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝜒″ )
6	3	simplbi	⊢ ( 𝜂 → 𝑖 ∈ 𝑛 )
7	6	bnj708	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑖 ∈ 𝑛 )
8	1	bnj1232	⊢ ( 𝜒 → 𝑛 ∈ 𝐷 )
9	8	bnj706	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑛 ∈ 𝐷 )
10	4	bnj923	⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
11	9 10	syl	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑛 ∈ ω )
12		elnn	⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω ) → 𝑖 ∈ ω )
13	7 11 12	syl2anc	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑖 ∈ ω )
14	2	simp3bi	⊢ ( 𝜏 → 𝑝 = suc 𝑛 )
15	14	bnj707	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝑝 = suc 𝑛 )
16		nnord	⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
17		ordsucelsuc	⊢ ( Ord 𝑛 → ( 𝑖 ∈ 𝑛 ↔ suc 𝑖 ∈ suc 𝑛 ) )
18	10 16 17	3syl	⊢ ( 𝑛 ∈ 𝐷 → ( 𝑖 ∈ 𝑛 ↔ suc 𝑖 ∈ suc 𝑛 ) )
19	18	biimpa	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) → suc 𝑖 ∈ suc 𝑛 )
20		eleq2	⊢ ( 𝑝 = suc 𝑛 → ( suc 𝑖 ∈ 𝑝 ↔ suc 𝑖 ∈ suc 𝑛 ) )
21	19 20	anim12i	⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) ∧ 𝑝 = suc 𝑛 ) → ( suc 𝑖 ∈ suc 𝑛 ∧ ( suc 𝑖 ∈ 𝑝 ↔ suc 𝑖 ∈ suc 𝑛 ) ) )
22	9 7 15 21	syl21anc	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( suc 𝑖 ∈ suc 𝑛 ∧ ( suc 𝑖 ∈ 𝑝 ↔ suc 𝑖 ∈ suc 𝑛 ) ) )
23		bianir	⊢ ( ( suc 𝑖 ∈ suc 𝑛 ∧ ( suc 𝑖 ∈ 𝑝 ↔ suc 𝑖 ∈ suc 𝑛 ) ) → suc 𝑖 ∈ 𝑝 )
24	22 23	syl	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → suc 𝑖 ∈ 𝑝 )
25	5 13 24	3jca	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) )

Metamath Proof Explorer

Theorem bnj1001

Proof