Theorem ordsucss

Description: The successor of an element of an ordinal class is a subset of it. (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 𝐴 ⊆ 𝐵 ) )