Metamath Proof Explorer


Theorem ominfOLD

Description: Obsolete version of ominf as of 2-Jan-2025. (Contributed by NM, 2-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ominfOLD ¬ ω Fin

Proof

Step Hyp Ref Expression
1 isfi ω Fin x ω ω x
2 nnord x ω Ord x
3 ordom Ord ω
4 ordelssne Ord x Ord ω x ω x ω x ω
5 2 3 4 sylancl x ω x ω x ω x ω
6 5 ibi x ω x ω x ω
7 df-pss x ω x ω x ω
8 6 7 sylibr x ω x ω
9 ensym ω x x ω
10 pssinf x ω x ω ¬ ω Fin
11 8 9 10 syl2an x ω ω x ¬ ω Fin
12 11 rexlimiva x ω ω x ¬ ω Fin
13 1 12 sylbi ω Fin ¬ ω Fin
14 pm2.01 ω Fin ¬ ω Fin ¬ ω Fin
15 13 14 ax-mp ¬ ω Fin