Theorem dfom5b

Description: A quantifier-free definition of _om that does not depend on ax-inf . (Note: label was changed from dfom5 to dfom5b to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	dfom5b	⊢ ω = ( On ∩ ∩ Limits )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	elint	⊢ ( 𝑥 ∈ ∩ Limits ↔ ∀ 𝑦 ( 𝑦 ∈ Limits → 𝑥 ∈ 𝑦 ) )
3		vex	⊢ 𝑦 ∈ V
4	3	ellimits	⊢ ( 𝑦 ∈ Limits ↔ Lim 𝑦 )
5	4	imbi1i	⊢ ( ( 𝑦 ∈ Limits → 𝑥 ∈ 𝑦 ) ↔ ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) )
6	5	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ Limits → 𝑥 ∈ 𝑦 ) ↔ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) )
7	2 6	bitr2i	⊢ ( ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) ↔ 𝑥 ∈ ∩ Limits )
8	7	anbi2i	⊢ ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ ∩ Limits ) )
9		elom	⊢ ( 𝑥 ∈ ω ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) ) )
10		elin	⊢ ( 𝑥 ∈ ( On ∩ ∩ Limits ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ∈ ∩ Limits ) )
11	8 9 10	3bitr4i	⊢ ( 𝑥 ∈ ω ↔ 𝑥 ∈ ( On ∩ ∩ Limits ) )
12	11	eqriv	⊢ ω = ( On ∩ ∩ Limits )