This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ⊆ 𝐵 → ¬ 𝐵 ∈ 𝐴 )