Theorem onssneli

Description: An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994)

	Ref	Expression
Hypothesis	on.1	⊢ 𝐴 ∈ On
Assertion	onssneli	⊢ ( 𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		on.1	⊢ 𝐴 ∈ On
2		ssel	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐵 ) )
3	1	oneli	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ On )
4		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
5		ordirr	⊢ ( Ord 𝐵 → ¬ 𝐵 ∈ 𝐵 )
6	3 4 5	3syl	⊢ ( 𝐵 ∈ 𝐴 → ¬ 𝐵 ∈ 𝐵 )
7	2 6	nsyli	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ∈ 𝐴 → ¬ 𝐵 ∈ 𝐴 ) )
8	7	pm2.01d	⊢ ( 𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴 )