This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1071

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
	Hypothesis	bnj1071.7	⊢ 𝐷 = ( ω ∖ { ∅ } )
	Assertion	bnj1071	⊢ ( 𝑛 ∈ 𝐷 → E Fr 𝑛 )

Proof

Step	Hyp	Ref	Expression
1		bnj1071.7	⊢ 𝐷 = ( ω ∖ { ∅ } )
2	1	bnj923	⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
3		nnord	⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
4		ordfr	⊢ ( Ord 𝑛 → E Fr 𝑛 )
5	2 3 4	3syl	⊢ ( 𝑛 ∈ 𝐷 → E Fr 𝑛 )