chnso

Description: A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025)

		Ref	Expression
	Assertion	chnso	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to \underset{˙}{<} Or ran C$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to \|C\| = \|C\|$
2		ischn	$⊢ C \in {Chain}_{A} \underset{˙}{<} \leftrightarrow (C \in Word A \land \forall n \in (dom C ∖ \{0\}) C (n - 1) \underset{˙}{<} C (n))$
3	2	bilani	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to (C \in Word A \land \forall n \in (dom C ∖ \{0\}) C (n - 1) \underset{˙}{<} C (n))$
4	3	simpld	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to C \in Word A$
5	1 4	wrdfd	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to C : (0 ..^\|C\|) ⟶ A$
6	5	frnd	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to ran C \subseteq A$
7		simpl	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to \underset{˙}{<} Po A$
8		poss	$⊢ ran C \subseteq A \to (\underset{˙}{<} Po A \to \underset{˙}{<} Po ran C)$
9	6 7 8	sylc	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to \underset{˙}{<} Po ran C$
10		fzossz	$⊢ (0 ..^\|C\|) \subseteq ℤ$
11		simp-4r	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to i \in (0 ..^\|C\|)$
12	10 11	sselid	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to i \in ℤ$
13	12	zred	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to i \in ℝ$
14		simplr	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to j \in (0 ..^\|C\|)$
15	10 14	sselid	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to j \in ℤ$
16	15	zred	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to j \in ℝ$
17	13 16	lttri4d	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to (i < j \lor i = j \lor j < i)$
18		simp-8l	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to \underset{˙}{<} Po A$
19		simp-8r	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to C \in {Chain}_{A} \underset{˙}{<}$
20		simpllr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to j \in (0 ..^\|C\|)$
21		elfzouz	$⊢ i \in (0 ..^\|C\|) \to i \in ℤ_{\geq 0}$
22	21	ad5antlr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to i \in ℤ_{\geq 0}$
23	15	adantr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to j \in ℤ$
24		simpr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to i < j$
25		elfzo2	$⊢ i \in (0 ..^j) \leftrightarrow (i \in ℤ_{\geq 0} \land j \in ℤ \land i < j)$
26	22 23 24 25	syl3anbrc	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to i \in (0 ..^j)$
27	18 19 20 26	chnlt	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to C (i) \underset{˙}{<} C (j)$
28		simp-4r	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to C (i) = x$
29		simplr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to C (j) = y$
30	27 28 29	3brtr3d	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i < j) \to x \underset{˙}{<} y$
31	30	ex	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to (i < j \to x \underset{˙}{<} y)$
32		simpr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i = j) \to i = j$
33	32	fveq2d	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i = j) \to C (i) = C (j)$
34		simp-4r	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i = j) \to C (i) = x$
35		simplr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i = j) \to C (j) = y$
36	33 34 35	3eqtr3d	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land i = j) \to x = y$
37	36	ex	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to (i = j \to x = y)$
38		simp-8l	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to \underset{˙}{<} Po A$
39		simp-8r	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to C \in {Chain}_{A} \underset{˙}{<}$
40	11	adantr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to i \in (0 ..^\|C\|)$
41		elfzouz	$⊢ j \in (0 ..^\|C\|) \to j \in ℤ_{\geq 0}$
42	41	ad3antlr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to j \in ℤ_{\geq 0}$
43	12	adantr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to i \in ℤ$
44		simpr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to j < i$
45		elfzo2	$⊢ j \in (0 ..^i) \leftrightarrow (j \in ℤ_{\geq 0} \land i \in ℤ \land j < i)$
46	42 43 44 45	syl3anbrc	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to j \in (0 ..^i)$
47	38 39 40 46	chnlt	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to C (j) \underset{˙}{<} C (i)$
48		simplr	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to C (j) = y$
49		simp-4r	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to C (i) = x$
50	47 48 49	3brtr3d	$⊢ ((((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \land j < i) \to y \underset{˙}{<} x$
51	50	ex	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to (j < i \to y \underset{˙}{<} x)$
52	31 37 51	3orim123d	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to ((i < j \lor i = j \lor j < i) \to (x \underset{˙}{<} y \lor x = y \lor y \underset{˙}{<} x))$
53	17 52	mpd	$⊢ (((((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \land j \in (0 ..^\|C\|)) \land C (j) = y) \to (x \underset{˙}{<} y \lor x = y \lor y \underset{˙}{<} x)$
54	5	ffnd	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to C Fn (0 ..^\|C\|)$
55	54	ad4antr	$⊢ (((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \to C Fn (0 ..^\|C\|)$
56		simpllr	$⊢ (((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \to y \in ran C$
57		fvelrnb	$⊢ C Fn (0 ..^\|C\|) \to (y \in ran C \leftrightarrow \exists j \in (0 ..^\|C\|) C (j) = y)$
58	57	biimpa	$⊢ (C Fn (0 ..^\|C\|) \land y \in ran C) \to \exists j \in (0 ..^\|C\|) C (j) = y$
59	55 56 58	syl2anc	$⊢ (((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \to \exists j \in (0 ..^\|C\|) C (j) = y$
60	53 59	r19.29a	$⊢ (((((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \land i \in (0 ..^\|C\|)) \land C (i) = x) \to (x \underset{˙}{<} y \lor x = y \lor y \underset{˙}{<} x)$
61	54	ad2antrr	$⊢ (((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \to C Fn (0 ..^\|C\|)$
62		simplr	$⊢ (((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \to x \in ran C$
63		fvelrnb	$⊢ C Fn (0 ..^\|C\|) \to (x \in ran C \leftrightarrow \exists i \in (0 ..^\|C\|) C (i) = x)$
64	63	biimpa	$⊢ (C Fn (0 ..^\|C\|) \land x \in ran C) \to \exists i \in (0 ..^\|C\|) C (i) = x$
65	61 62 64	syl2anc	$⊢ (((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \to \exists i \in (0 ..^\|C\|) C (i) = x$
66	60 65	r19.29a	$⊢ (((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land x \in ran C) \land y \in ran C) \to (x \underset{˙}{<} y \lor x = y \lor y \underset{˙}{<} x)$
67	66	anasss	$⊢ ((\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \land (x \in ran C \land y \in ran C)) \to (x \underset{˙}{<} y \lor x = y \lor y \underset{˙}{<} x)$
68	9 67	issod	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to \underset{˙}{<} Or ran C$

Metamath Proof Explorer

Theorem chnso

Proof