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 𝐴 → ( 𝐵 ∈ ( 𝐴 ∖ 1o ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ) )

Proof

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