Theorem ordsucsssuc

Description: The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003)

	Ref	Expression
Assertion	ordsucsssuc	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ordsucelsuc	⊢ ( Ord 𝐴 → ( 𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ suc 𝐴 ) )
2	1	notbid	⊢ ( Ord 𝐴 → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ suc 𝐵 ∈ suc 𝐴 ) )
3	2	adantr	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ suc 𝐵 ∈ suc 𝐴 ) )
4		ordtri1	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 ) )
5		ordsuc	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
6		ordsuc	⊢ ( Ord 𝐵 ↔ Ord suc 𝐵 )
7		ordtri1	⊢ ( ( Ord suc 𝐴 ∧ Ord suc 𝐵 ) → ( suc 𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ suc 𝐴 ) )
8	5 6 7	syl2anb	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( suc 𝐴 ⊆ suc 𝐵 ↔ ¬ suc 𝐵 ∈ suc 𝐴 ) )
9	3 4 8	3bitr4d	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵 ) )