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