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 𝖫𝗂𝗆𝗂𝗍𝗌

Proof

Step Hyp Ref Expression
1 vex x V
2 1 elint x 𝖫𝗂𝗆𝗂𝗍𝗌 y y 𝖫𝗂𝗆𝗂𝗍𝗌 x y
3 vex y V
4 3 ellimits y 𝖫𝗂𝗆𝗂𝗍𝗌 Lim y
5 4 imbi1i y 𝖫𝗂𝗆𝗂𝗍𝗌 x y Lim y x y
6 5 albii y y 𝖫𝗂𝗆𝗂𝗍𝗌 x y y Lim y x y
7 2 6 bitr2i y Lim y x y x 𝖫𝗂𝗆𝗂𝗍𝗌
8 7 anbi2i x On y Lim y x y x On x 𝖫𝗂𝗆𝗂𝗍𝗌
9 elom x ω x On y Lim y x y
10 elin x On 𝖫𝗂𝗆𝗂𝗍𝗌 x On x 𝖫𝗂𝗆𝗂𝗍𝗌
11 8 9 10 3bitr4i x ω x On 𝖫𝗂𝗆𝗂𝗍𝗌
12 11 eqriv ω = On 𝖫𝗂𝗆𝗂𝗍𝗌