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	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj970.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
Assertion	bnj970	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑝 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		bnj970.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
2		bnj970.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
3	1	bnj1232	⊢ ( 𝜒 → 𝑛 ∈ 𝐷 )
4	3	3ad2ant1	⊢ ( ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) → 𝑛 ∈ 𝐷 )
5	4	adantl	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑛 ∈ 𝐷 )
6		simpr3	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑝 = suc 𝑛 )
7	2	bnj923	⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
8		peano2	⊢ ( 𝑛 ∈ ω → suc 𝑛 ∈ ω )
9		eleq1	⊢ ( 𝑝 = suc 𝑛 → ( 𝑝 ∈ ω ↔ suc 𝑛 ∈ ω ) )
10		bianir	⊢ ( ( suc 𝑛 ∈ ω ∧ ( 𝑝 ∈ ω ↔ suc 𝑛 ∈ ω ) ) → 𝑝 ∈ ω )
11	8 9 10	syl2an	⊢ ( ( 𝑛 ∈ ω ∧ 𝑝 = suc 𝑛 ) → 𝑝 ∈ ω )
12	7 11	sylan	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ) → 𝑝 ∈ ω )
13		df-suc	⊢ suc 𝑛 = ( 𝑛 ∪ { 𝑛 } )
14	13	eqeq2i	⊢ ( 𝑝 = suc 𝑛 ↔ 𝑝 = ( 𝑛 ∪ { 𝑛 } ) )
15		ssun2	⊢ { 𝑛 } ⊆ ( 𝑛 ∪ { 𝑛 } )
16		vex	⊢ 𝑛 ∈ V
17	16	snnz	⊢ { 𝑛 } ≠ ∅
18		ssn0	⊢ ( ( { 𝑛 } ⊆ ( 𝑛 ∪ { 𝑛 } ) ∧ { 𝑛 } ≠ ∅ ) → ( 𝑛 ∪ { 𝑛 } ) ≠ ∅ )
19	15 17 18	mp2an	⊢ ( 𝑛 ∪ { 𝑛 } ) ≠ ∅
20		neeq1	⊢ ( 𝑝 = ( 𝑛 ∪ { 𝑛 } ) → ( 𝑝 ≠ ∅ ↔ ( 𝑛 ∪ { 𝑛 } ) ≠ ∅ ) )
21	19 20	mpbiri	⊢ ( 𝑝 = ( 𝑛 ∪ { 𝑛 } ) → 𝑝 ≠ ∅ )
22	14 21	sylbi	⊢ ( 𝑝 = suc 𝑛 → 𝑝 ≠ ∅ )
23	22	adantl	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ) → 𝑝 ≠ ∅ )
24	2	eleq2i	⊢ ( 𝑝 ∈ 𝐷 ↔ 𝑝 ∈ ( ω ∖ { ∅ } ) )
25		eldifsn	⊢ ( 𝑝 ∈ ( ω ∖ { ∅ } ) ↔ ( 𝑝 ∈ ω ∧ 𝑝 ≠ ∅ ) )
26	24 25	bitri	⊢ ( 𝑝 ∈ 𝐷 ↔ ( 𝑝 ∈ ω ∧ 𝑝 ≠ ∅ ) )
27	12 23 26	sylanbrc	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑝 = suc 𝑛 ) → 𝑝 ∈ 𝐷 )
28	5 6 27	syl2anc	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝜒 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ) → 𝑝 ∈ 𝐷 )

Metamath Proof Explorer

Theorem bnj970

Proof