Theorem chninf

Description: There is an infinite number of chains for any infinite alphabet and any relation. For instance, all the singletons of alphabet characters match. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Assertion	chninf	|- ( A e/ Fin -> ( .< Chain A ) e/ Fin )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( y e. A -> y e. A )
2	1	s1chn	|- ( y e. A -> <" y "> e. ( .< Chain A ) )
3	2	rgen	|- A. y e. A <" y "> e. ( .< Chain A )
4		s111	|- ( ( y e. A /\ x e. A ) -> ( <" y "> = <" x "> <-> y = x ) )
5	4	biimpd	|- ( ( y e. A /\ x e. A ) -> ( <" y "> = <" x "> -> y = x ) )
6	5	rgen2	|- A. y e. A A. x e. A ( <" y "> = <" x "> -> y = x )
7	3 6	pm3.2i	|- ( A. y e. A <" y "> e. ( .< Chain A ) /\ A. y e. A A. x e. A ( <" y "> = <" x "> -> y = x ) )
8		eqid	|- ( y e. A |-> <" y "> ) = ( y e. A |-> <" y "> )
9		s1eq	|- ( y = x -> <" y "> = <" x "> )
10	8 9	f1mpt	|- ( ( y e. A |-> <" y "> ) : A -1-1-> ( .< Chain A ) <-> ( A. y e. A <" y "> e. ( .< Chain A ) /\ A. y e. A A. x e. A ( <" y "> = <" x "> -> y = x ) ) )
11	7 10	mpbir	|- ( y e. A |-> <" y "> ) : A -1-1-> ( .< Chain A )
12		f1fi	|- ( ( ( .< Chain A ) e. Fin /\ ( y e. A |-> <" y "> ) : A -1-1-> ( .< Chain A ) ) -> A e. Fin )
13	11 12	mpan2	|- ( ( .< Chain A ) e. Fin -> A e. Fin )
14	13	a1i	|- ( T. -> ( ( .< Chain A ) e. Fin -> A e. Fin ) )
15	14	nelcon3d	|- ( T. -> ( A e/ Fin -> ( .< Chain A ) e/ Fin ) )
16	15	mptru	|- ( A e/ Fin -> ( .< Chain A ) e/ Fin )