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 
|- _om = ( On i^i |^| Limits )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 elint 
 |-  ( x e. |^| Limits <-> A. y ( y e. Limits -> x e. y ) )
3 vex 
 |-  y e. _V
4 3 ellimits 
 |-  ( y e. Limits <-> Lim y )
5 4 imbi1i 
 |-  ( ( y e. Limits -> x e. y ) <-> ( Lim y -> x e. y ) )
6 5 albii 
 |-  ( A. y ( y e. Limits -> x e. y ) <-> A. y ( Lim y -> x e. y ) )
7 2 6 bitr2i 
 |-  ( A. y ( Lim y -> x e. y ) <-> x e. |^| Limits )
8 7 anbi2i 
 |-  ( ( x e. On /\ A. y ( Lim y -> x e. y ) ) <-> ( x e. On /\ x e. |^| Limits ) )
9 elom 
 |-  ( x e. _om <-> ( x e. On /\ A. y ( Lim y -> x e. y ) ) )
10 elin 
 |-  ( x e. ( On i^i |^| Limits ) <-> ( x e. On /\ x e. |^| Limits ) )
11 8 9 10 3bitr4i 
 |-  ( x e. _om <-> x e. ( On i^i |^| Limits ) )
12 11 eqriv 
 |-  _om = ( On i^i |^| Limits )