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	|- -. _om e. Fin

Proof

Step	Hyp	Ref	Expression
1		isfi	|- ( _om e. Fin <-> E. x e. _om _om ~~ x )
2		nnord	|- ( x e. _om -> Ord x )
3		ordom	|- Ord _om
4		ordelssne	|- ( ( Ord x /\ Ord _om ) -> ( x e. _om <-> ( x C_ _om /\ x =/= _om ) ) )
5	2 3 4	sylancl	|- ( x e. _om -> ( x e. _om <-> ( x C_ _om /\ x =/= _om ) ) )
6	5	ibi	|- ( x e. _om -> ( x C_ _om /\ x =/= _om ) )
7		df-pss	|- ( x C. _om <-> ( x C_ _om /\ x =/= _om ) )
8	6 7	sylibr	|- ( x e. _om -> x C. _om )
9		ensym	|- ( _om ~~ x -> x ~~ _om )
10		pssinf	|- ( ( x C. _om /\ x ~~ _om ) -> -. _om e. Fin )
11	8 9 10	syl2an	|- ( ( x e. _om /\ _om ~~ x ) -> -. _om e. Fin )
12	11	rexlimiva	|- ( E. x e. _om _om ~~ x -> -. _om e. Fin )
13	1 12	sylbi	|- ( _om e. Fin -> -. _om e. Fin )
14		pm2.01	|- ( ( _om e. Fin -> -. _om e. Fin ) -> -. _om e. Fin )
15	13 14	ax-mp	|- -. _om e. Fin