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

Metamath Proof Explorer

Theorem ordsucss

Description: The successor of an element of an ordinal class is a subset of it. Lemma 1.14 of Schloeder p. 2. (Contributed by NM, 21-Jun-1998)

Ref Expression
Assertion ordsucss ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ordelord ⊢ ( ( Ord 𝐵 ∧ 𝐴 ∈ 𝐵 ) → Ord 𝐴 )
2 ordnbtwn ⊢ ( Ord 𝐴 → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) )
3 imnan ⊢ ( ( 𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴 ) ↔ ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) )
4 2 3 sylibr ⊢ ( Ord 𝐴 → ( 𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴 ) )
5 4 adantr ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴 ) )
6 ordsuc ⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
7 ordtri1 ⊢ ( ( Ord suc 𝐴 ∧ Ord 𝐵 ) → ( suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴 ) )
8 6 7 sylanb ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴 ) )
9 5 8 sylibrd ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
10 1 9 sylan ⊢ ( ( ( Ord 𝐵 ∧ 𝐴 ∈ 𝐵 ) ∧ Ord 𝐵 ) → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
11 10 exp31 ⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) ) ) )
12 11 pm2.43b ⊢ ( 𝐴 ∈ 𝐵 → ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) ) )
13 12 pm2.43b ⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )