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