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 𝐵 ) )