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

Metamath Proof Explorer

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 )