Metamath Proof Explorer

Theorem nulchn

Description: Empty set is an increasing chain for every range and every relation. (Contributed by Ender Ting, 19-Nov-2024) (Revised by Ender Ting, 17-Jan-2026)

Ref Expression
Assertion nulchn ⊢ ∅ ∈ Chain A < ˙

Proof

Step Hyp Ref Expression
1 wrd0 ⊢ ∅ ∈ Word A
2 dm0 ⊢ dom ⁡ ∅ = ∅
3 2 difeq1i ⊢ dom ⁡ ∅ ∖ 0 = ∅ ∖ 0
4 0dif ⊢ ∅ ∖ 0 = ∅
5 3 4 eqtri ⊢ dom ⁡ ∅ ∖ 0 = ∅
6 rzal ⊢ dom ⁡ ∅ ∖ 0 = ∅ → ∀ x ∈ dom ⁡ ∅ ∖ 0 ∅ ⁡ x − 1 < ˙ ∅ ⁡ x
7 5 6 ax-mp ⊢ ∀ x ∈ dom ⁡ ∅ ∖ 0 ∅ ⁡ x − 1 < ˙ ∅ ⁡ x
8 1 7 pm3.2i ⊢ ∅ ∈ Word A ∧ ∀ x ∈ dom ⁡ ∅ ∖ 0 ∅ ⁡ x − 1 < ˙ ∅ ⁡ x
9 ischn ⊢ ∅ ∈ Chain A < ˙ ↔ ∅ ∈ Word A ∧ ∀ x ∈ dom ⁡ ∅ ∖ 0 ∅ ⁡ x − 1 < ˙ ∅ ⁡ x
10 8 9 mpbir ⊢ ∅ ∈ Chain A < ˙