Theorem s1chn

Description: A singleton word is always a chain. (Contributed by Thierry Arnoux, 19-Oct-2025)

	Ref	Expression
Hypothesis	s1chn.1	|- ( ph -> X e. A )
Assertion	s1chn	|- ( ph -> <" X "> e. ( .< Chain A ) )

Proof

Step	Hyp	Ref	Expression
1		s1chn.1	|- ( ph -> X e. A )
2	1	s1cld	|- ( ph -> <" X "> e. Word A )
3		ral0	|- A. n e. (/) ( <" X "> ` ( n - 1 ) ) .< ( <" X "> ` n )
4		s1dm	|- dom <" X "> = { 0 }
5	4	difeq1i	|- ( dom <" X "> \ { 0 } ) = ( { 0 } \ { 0 } )
6		difid	|- ( { 0 } \ { 0 } ) = (/)
7	5 6	eqtri	|- ( dom <" X "> \ { 0 } ) = (/)
8	7	raleqi	|- ( A. n e. ( dom <" X "> \ { 0 } ) ( <" X "> ` ( n - 1 ) ) .< ( <" X "> ` n ) <-> A. n e. (/) ( <" X "> ` ( n - 1 ) ) .< ( <" X "> ` n ) )
9	3 8	mpbir	|- A. n e. ( dom <" X "> \ { 0 } ) ( <" X "> ` ( n - 1 ) ) .< ( <" X "> ` n )
10		ischn	|- ( <" X "> e. ( .< Chain A ) <-> ( <" X "> e. Word A /\ A. n e. ( dom <" X "> \ { 0 } ) ( <" X "> ` ( n - 1 ) ) .< ( <" X "> ` n ) ) )
11	2 9 10	sylanblrc	|- ( ph -> <" X "> e. ( .< Chain A ) )