Metamath Proof Explorer

Theorem ordeldifsucon

Description: Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025)

Ref Expression
Assertion ordeldifsucon ⊢Ord⁡A∧B∈On→C∈A∖suc⁡B↔C∈A∧B∈C

Proof

Step Hyp Ref Expression
1 eldif ⊢C∈A∖suc⁡B↔C∈A∧¬C∈suc⁡B
2 simplr ⊢Ord⁡A∧B∈On∧C∈A→B∈On
3 ordelord ⊢Ord⁡A∧C∈A→Ord⁡C
4 3 adantlr ⊢Ord⁡A∧B∈On∧C∈A→Ord⁡C
5 ordelsuc ⊢B∈On∧Ord⁡C→B∈C↔suc⁡B⊆C
6 2 4 5 syl2anc ⊢Ord⁡A∧B∈On∧C∈A→B∈C↔suc⁡B⊆C
7 eloni ⊢B∈On→Ord⁡B
8 ordsuci ⊢Ord⁡B→Ord⁡suc⁡B
9 2 7 8 3syl ⊢Ord⁡A∧B∈On∧C∈A→Ord⁡suc⁡B
10 ordtri1 ⊢Ord⁡suc⁡B∧Ord⁡C→suc⁡B⊆C↔¬C∈suc⁡B
11 9 4 10 syl2anc ⊢Ord⁡A∧B∈On∧C∈A→suc⁡B⊆C↔¬C∈suc⁡B
12 6 11 bitr2d ⊢Ord⁡A∧B∈On∧C∈A→¬C∈suc⁡B↔B∈C
13 12 pm5.32da ⊢Ord⁡A∧B∈On→C∈A∧¬C∈suc⁡B↔C∈A∧B∈C
14 1 13 bitrid ⊢Ord⁡A∧B∈On→C∈A∖suc⁡B↔C∈A∧B∈C