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	biimpi	$⊢ 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	adantl	$⊢ (\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))$
5	4	simpld	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to C \in Word A$
6	1 5	wrdfd	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to C : (0 ..^\|C\|) ⟶ A$
7	6	frnd	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to ran C \subseteq A$
8		simpl	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to \underset{˙}{<} Po A$
9		poss	$⊢ ran C \subseteq A \to (\underset{˙}{<} Po A \to \underset{˙}{<} Po ran C)$
10	7 8 9	sylc	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to \underset{˙}{<} Po ran C$
11		fzossz	$⊢ (0 ..^\|C\|) \subseteq ℤ$
12		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\|)$
13	11 12	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 ℤ$
14	13	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 ℝ$
15		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\|)$
16	11 15	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 ℤ$
17	16	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 ℝ$
18	14 17	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)$
19		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$
20		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{˙}{<}$
21		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\|)$
22		elfzouz	$⊢ i \in (0 ..^\|C\|) \to i \in ℤ_{\geq 0}$
23	22	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}$
24	16	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 ℤ$
25		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$
26		elfzo2	$⊢ i \in (0 ..^j) \leftrightarrow (i \in ℤ_{\geq 0} \land j \in ℤ \land i < j)$
27	23 24 25 26	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)$
28	19 20 21 27	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)$
29		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$
30		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$
31	28 29 30	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$
32	31	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)$
33		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$
34	33	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)$
35		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$
36		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$
37	34 35 36	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$
38	37	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)$
39		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$
40		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{˙}{<}$
41	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 (0 ..^\|C\|)$
42		elfzouz	$⊢ j \in (0 ..^\|C\|) \to j \in ℤ_{\geq 0}$
43	42	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}$
44	13	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 ℤ$
45		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$
46		elfzo2	$⊢ j \in (0 ..^i) \leftrightarrow (j \in ℤ_{\geq 0} \land i \in ℤ \land j < i)$
47	43 44 45 46	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)$
48	39 40 41 47	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)$
49		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$
50		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$
51	48 49 50	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$
52	51	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)$
53	32 38 52	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))$
54	18 53	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)$
55	6	ffnd	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to C Fn (0 ..^\|C\|)$
56	55	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\|)$
57		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$
58		fvelrnb	$⊢ C Fn (0 ..^\|C\|) \to (y \in ran C \leftrightarrow \exists j \in (0 ..^\|C\|) C (j) = y)$
59	58	biimpa	$⊢ (C Fn (0 ..^\|C\|) \land y \in ran C) \to \exists j \in (0 ..^\|C\|) C (j) = y$
60	56 57 59	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$
61	54 60	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)$
62	55	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\|)$
63		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$
64		fvelrnb	$⊢ C Fn (0 ..^\|C\|) \to (x \in ran C \leftrightarrow \exists i \in (0 ..^\|C\|) C (i) = x)$
65	64	biimpa	$⊢ (C Fn (0 ..^\|C\|) \land x \in ran C) \to \exists i \in (0 ..^\|C\|) C (i) = x$
66	62 63 65	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$
67	61 66	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)$
68	67	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)$
69	10 68	issod	$⊢ (\underset{˙}{<} Po A \land C \in {Chain}_{A} \underset{˙}{<}) \to \underset{˙}{<} Or ran C$

Metamath Proof Explorer

Theorem chnso

Proof