Metamath Proof Explorer

Theorem ordeldif1o

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

Ref Expression
Assertion ordeldif1o ⊢ Ord ⁡ A → B ∈ A ∖ 1 𝑜 ↔ B ∈ A ∧ B ≠ ∅

Proof

Step Hyp Ref Expression
1 df-1o ⊢ 1 𝑜 = suc ⁡ ∅
2 1 difeq2i ⊢ A ∖ 1 𝑜 = A ∖ suc ⁡ ∅
3 2 eleq2i ⊢ B ∈ A ∖ 1 𝑜 ↔ B ∈ A ∖ suc ⁡ ∅
4 eldif ⊢ B ∈ A ∖ suc ⁡ ∅ ↔ B ∈ A ∧ ¬ B ∈ suc ⁡ ∅
5 3 4 bitri ⊢ B ∈ A ∖ 1 𝑜 ↔ B ∈ A ∧ ¬ B ∈ suc ⁡ ∅
6 0elon ⊢ ∅ ∈ On
7 ordelord ⊢ Ord ⁡ A ∧ B ∈ A → Ord ⁡ B
8 ordelsuc ⊢ ∅ ∈ On ∧ Ord ⁡ B → ∅ ∈ B ↔ suc ⁡ ∅ ⊆ B
9 6 7 8 sylancr ⊢ Ord ⁡ A ∧ B ∈ A → ∅ ∈ B ↔ suc ⁡ ∅ ⊆ B
10 ord0eln0 ⊢ Ord ⁡ B → ∅ ∈ B ↔ B ≠ ∅
11 7 10 syl ⊢ Ord ⁡ A ∧ B ∈ A → ∅ ∈ B ↔ B ≠ ∅
12 eloni ⊢ ∅ ∈ On → Ord ⁡ ∅
13 ordsuci ⊢ Ord ⁡ ∅ → Ord ⁡ suc ⁡ ∅
14 6 12 13 mp2b ⊢ Ord ⁡ suc ⁡ ∅
15 ordtri1 ⊢ Ord ⁡ suc ⁡ ∅ ∧ Ord ⁡ B → suc ⁡ ∅ ⊆ B ↔ ¬ B ∈ suc ⁡ ∅
16 14 7 15 sylancr ⊢ Ord ⁡ A ∧ B ∈ A → suc ⁡ ∅ ⊆ B ↔ ¬ B ∈ suc ⁡ ∅
17 9 11 16 3bitr3rd ⊢ Ord ⁡ A ∧ B ∈ A → ¬ B ∈ suc ⁡ ∅ ↔ B ≠ ∅
18 17 pm5.32da ⊢ Ord ⁡ A → B ∈ A ∧ ¬ B ∈ suc ⁡ ∅ ↔ B ∈ A ∧ B ≠ ∅
19 5 18 bitrid ⊢ Ord ⁡ A → B ∈ A ∖ 1 𝑜 ↔ B ∈ A ∧ B ≠ ∅