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

Metamath Proof Explorer

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