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 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		wrd0	⊢ ∅ ∈ Word 𝐴
2		dm0	⊢ dom ∅ = ∅
3	2	difeq1i	⊢ ( dom ∅ ∖ { 0 } ) = ( ∅ ∖ { 0 } )
4		0dif	⊢ ( ∅ ∖ { 0 } ) = ∅
5	3 4	eqtri	⊢ ( dom ∅ ∖ { 0 } ) = ∅
6		rzal	⊢ ( ( dom ∅ ∖ { 0 } ) = ∅ → ∀ 𝑥 ∈ ( dom ∅ ∖ { 0 } ) ( ∅ ‘ ( 𝑥 − 1 ) ) < ( ∅ ‘ 𝑥 ) )
7	5 6	ax-mp	⊢ ∀ 𝑥 ∈ ( dom ∅ ∖ { 0 } ) ( ∅ ‘ ( 𝑥 − 1 ) ) < ( ∅ ‘ 𝑥 )
8	1 7	pm3.2i	⊢ ( ∅ ∈ Word 𝐴 ∧ ∀ 𝑥 ∈ ( dom ∅ ∖ { 0 } ) ( ∅ ‘ ( 𝑥 − 1 ) ) < ( ∅ ‘ 𝑥 ) )
9		ischn	⊢ ( ∅ ∈ ( < Chain 𝐴 ) ↔ ( ∅ ∈ Word 𝐴 ∧ ∀ 𝑥 ∈ ( dom ∅ ∖ { 0 } ) ( ∅ ‘ ( 𝑥 − 1 ) ) < ( ∅ ‘ 𝑥 ) ) )
10	8 9	mpbir	⊢ ∅ ∈ ( < Chain 𝐴 )