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

Metamath Proof Explorer

Theorem ordsssuc2

Description: An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion ordsssuc2 ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elong ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ On ↔ Ord 𝐴 ) )
2 1 biimprd ⊢ ( 𝐴 ∈ V → ( Ord 𝐴 → 𝐴 ∈ On ) )
3 2 anim1d ⊢ ( 𝐴 ∈ V → ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ) )
4 onsssuc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )
5 3 4 syl6 ⊢ ( 𝐴 ∈ V → ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) ) )
6 annim ⊢ ( ( 𝐵 ∈ On ∧ ¬ 𝐴 ∈ V ) ↔ ¬ ( 𝐵 ∈ On → 𝐴 ∈ V ) )
7 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ On ) → 𝐴 ∈ V )
8 7 ex ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ∈ On → 𝐴 ∈ V ) )
9 elex ⊢ ( 𝐴 ∈ suc 𝐵 → 𝐴 ∈ V )
10 9 a1d ⊢ ( 𝐴 ∈ suc 𝐵 → ( 𝐵 ∈ On → 𝐴 ∈ V ) )
11 8 10 pm5.21ni ⊢ ( ¬ ( 𝐵 ∈ On → 𝐴 ∈ V ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )
12 6 11 sylbi ⊢ ( ( 𝐵 ∈ On ∧ ¬ 𝐴 ∈ V ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )
13 12 expcom ⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ∈ On → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) ) )
14 13 adantld ⊢ ( ¬ 𝐴 ∈ V → ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) ) )
15 5 14 pm2.61i ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )