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

Metamath Proof Explorer

Theorem dfom5

Description: _om is the smallest limit ordinal and can be defined as such (although the Axiom of Infinity is needed to ensure that at least one limit ordinal exists). Theorem 1.23 of Schloeder p. 4. (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 2-Feb-2013)

		Ref	Expression
	Assertion	dfom5	⊢ ω = ∩ { 𝑥 ∣ Lim 𝑥 }

Proof

Step	Hyp	Ref	Expression
1		elom3	⊢ ( 𝑦 ∈ ω ↔ ∀ 𝑥 ( Lim 𝑥 → 𝑦 ∈ 𝑥 ) )
2		vex	⊢ 𝑦 ∈ V
3	2	elintab	⊢ ( 𝑦 ∈ ∩ { 𝑥 ∣ Lim 𝑥 } ↔ ∀ 𝑥 ( Lim 𝑥 → 𝑦 ∈ 𝑥 ) )
4	1 3	bitr4i	⊢ ( 𝑦 ∈ ω ↔ 𝑦 ∈ ∩ { 𝑥 ∣ Lim 𝑥 } )
5	4	eqriv	⊢ ω = ∩ { 𝑥 ∣ Lim 𝑥 }