Metamath Proof Explorer

Theorem ordeldif

Description: Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025)

Ref Expression
Assertion ordeldif ⊢ Ord ⁡ A ∧ Ord ⁡ B → C ∈ A ∖ B ↔ C ∈ A ∧ B ⊆ C

Proof

Step Hyp Ref Expression
1 eldif ⊢ C ∈ A ∖ B ↔ C ∈ A ∧ ¬ C ∈ B
2 simpr ⊢ Ord ⁡ A ∧ Ord ⁡ B → Ord ⁡ B
3 ordelord ⊢ Ord ⁡ A ∧ C ∈ A → Ord ⁡ C
4 3 adantlr ⊢ Ord ⁡ A ∧ Ord ⁡ B ∧ C ∈ A → Ord ⁡ C
5 ordtri1 ⊢ Ord ⁡ B ∧ Ord ⁡ C → B ⊆ C ↔ ¬ C ∈ B
6 2 4 5 syl2an2r ⊢ Ord ⁡ A ∧ Ord ⁡ B ∧ C ∈ A → B ⊆ C ↔ ¬ C ∈ B
7 6 bicomd ⊢ Ord ⁡ A ∧ Ord ⁡ B ∧ C ∈ A → ¬ C ∈ B ↔ B ⊆ C
8 7 pm5.32da ⊢ Ord ⁡ A ∧ Ord ⁡ B → C ∈ A ∧ ¬ C ∈ B ↔ C ∈ A ∧ B ⊆ C
9 1 8 bitrid ⊢ Ord ⁡ A ∧ Ord ⁡ B → C ∈ A ∖ B ↔ C ∈ A ∧ B ⊆ C