chnso - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > chnso		Structured version Visualization version GIF version

Theorem chnso 18676

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

**Assertion**
Ref	Expression
chnso	⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Or ran 𝐶)

Proof of Theorem chnso Dummy variables 𝑥 𝑦 𝑖 𝑗 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2770	. . . . 5 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → (♯‘𝐶) = (♯‘𝐶))
2		ischn 18659	. . . . . . 7 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
3	2	bilani 509	. . . . . 6 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
4	3	simpld 499	. . . . 5 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶 ∈ Word 𝐴)
5	1, 4	wrdfd 14552	. . . 4 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶:(0..^(♯‘𝐶))⟶𝐴)
6	5	frnd 6712	. . 3 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → ran 𝐶 ⊆ 𝐴)
7		simpl 487	. . 3 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Po 𝐴)
8		poss 5569	. . 3 ⊢ (ran 𝐶 ⊆ 𝐴 → ( < Po 𝐴 → < Po ran 𝐶))
9	6, 7, 8	sylc 66	. 2 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Po ran 𝐶)
10		fzossz 13704	. . . . . . . . 9 ⊢ (0..^(♯‘𝐶)) ⊆ ℤ
11		simp-4r 795	. . . . . . . . 9 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ (0..^(♯‘𝐶)))
12	10, 11	sselid 3943	. . . . . . . 8 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ ℤ)
13	12	zred 12696	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ ℝ)
14		simplr 780	. . . . . . . . 9 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ (0..^(♯‘𝐶)))
15	10, 14	sselid 3943	. . . . . . . 8 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ ℤ)
16	15	zred 12696	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ ℝ)
17	13, 16	lttri4d 11347	. . . . . 6 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖))
18		simp-8l 802	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → < Po 𝐴)
19		simp-8r 803	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝐶 ∈ ( < Chain 𝐴))
20		simpllr 787	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (0..^(♯‘𝐶)))
21		elfzouz 13688	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0..^(♯‘𝐶)) → 𝑖 ∈ (ℤ_≥‘0))
22	21	ad5antlr 747	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 ∈ (ℤ_≥‘0))
23	15	adantr 485	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
24		simpr 489	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
25		elfzo2 13686	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0..^𝑗) ↔ (𝑖 ∈ (ℤ_≥‘0) ∧ 𝑗 ∈ ℤ ∧ 𝑖 < 𝑗))
26	22, 23, 24, 25	syl3anbrc 1360	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 ∈ (0..^𝑗))
27	18, 19, 20, 26	chnlt 18675	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑖) < (𝐶‘𝑗))
28		simp-4r 795	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑖) = 𝑥)
29		simplr 780	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑗) = 𝑦)
30	27, 28, 29	3brtr3d 5143	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑥 < 𝑦)
31	30	ex 417	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 < 𝑗 → 𝑥 < 𝑦))
32		simpr 489	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
33	32	fveq2d 6883	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑖) = (𝐶‘𝑗))
34		simp-4r 795	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑖) = 𝑥)
35		simplr 780	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑗) = 𝑦)
36	33, 34, 35	3eqtr3d 2812	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → 𝑥 = 𝑦)
37	36	ex 417	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 = 𝑗 → 𝑥 = 𝑦))
38		simp-8l 802	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → < Po 𝐴)
39		simp-8r 803	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝐶 ∈ ( < Chain 𝐴))
40	11	adantr 485	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑖 ∈ (0..^(♯‘𝐶)))
41		elfzouz 13688	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0..^(♯‘𝐶)) → 𝑗 ∈ (ℤ_≥‘0))
42	41	ad3antlr 743	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 ∈ (ℤ_≥‘0))
43	12	adantr 485	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑖 ∈ ℤ)
44		simpr 489	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 < 𝑖)
45		elfzo2 13686	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑖) ↔ (𝑗 ∈ (ℤ_≥‘0) ∧ 𝑖 ∈ ℤ ∧ 𝑗 < 𝑖))
46	42, 43, 44, 45	syl3anbrc 1360	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 ∈ (0..^𝑖))
47	38, 39, 40, 46	chnlt 18675	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑗) < (𝐶‘𝑖))
48		simplr 780	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑗) = 𝑦)
49		simp-4r 795	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑖) = 𝑥)
50	47, 48, 49	3brtr3d 5143	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑦 < 𝑥)
51	50	ex 417	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑗 < 𝑖 → 𝑦 < 𝑥))
52	31, 37, 51	3orim123d 1470	. . . . . 6 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → ((𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)))
53	17, 52	mpd 16	. . . . 5 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
54	5	ffnd 6704	. . . . . . 7 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶 Fn (0..^(♯‘𝐶)))
55	54	ad4antr 744	. . . . . 6 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → 𝐶 Fn (0..^(♯‘𝐶)))
56		simpllr 787	. . . . . 6 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → 𝑦 ∈ ran 𝐶)
57		fvelrnb 6939	. . . . . . 7 ⊢ (𝐶 Fn (0..^(♯‘𝐶)) → (𝑦 ∈ ran 𝐶 ↔ ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦))
58	57	biimpa 481	. . . . . 6 ⊢ ((𝐶 Fn (0..^(♯‘𝐶)) ∧ 𝑦 ∈ ran 𝐶) → ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦)
59	55, 56, 58	syl2anc 595	. . . . 5 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦)
60	53, 59	r19.29a 3179	. . . 4 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
61	54	ad2antrr 738	. . . . 5 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → 𝐶 Fn (0..^(♯‘𝐶)))
62		simplr 780	. . . . 5 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → 𝑥 ∈ ran 𝐶)
63		fvelrnb 6939	. . . . . 6 ⊢ (𝐶 Fn (0..^(♯‘𝐶)) → (𝑥 ∈ ran 𝐶 ↔ ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥))
64	63	biimpa 481	. . . . 5 ⊢ ((𝐶 Fn (0..^(♯‘𝐶)) ∧ 𝑥 ∈ ran 𝐶) → ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥)
65	61, 62, 64	syl2anc 595	. . . 4 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥)
66	60, 65	r19.29a 3179	. . 3 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
67	66	anasss 471	. 2 ⊢ ((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ (𝑥 ∈ ran 𝐶 ∧ 𝑦 ∈ ran 𝐶)) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
68	9, 67	issod 5602	1 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Or ran 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∨ w3o 1100 = wceq 1567 ∈ wcel 2149 ∀wral 3085 ∃wrex 3095 ∖ cdif 3910 ⊆ wss 3913 {csn 4591 class class class wbr 5110 Po wpo 5565 Or wor 5566 dom cdm 5659 ran crn 5660 Fn wfn 6528 ‘cfv 6533 (class class class)co 7408 0cc0 11096 1c1 11097 < clt 11239 − cmin 11437 ℤcz 12587 ℤ_≥cuz 12858 ..^cfzo 13678 ♯chash 14362 Word cword 14546 Chain cchn 18657

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-cnex 11152 ax-resscn 11153 ax-1cn 11154 ax-icn 11155 ax-addcl 11156 ax-addrcl 11157 ax-mulcl 11158 ax-mulrcl 11159 ax-mulcom 11160 ax-addass 11161 ax-mulass 11162 ax-distr 11163 ax-i2m1 11164 ax-1ne0 11165 ax-1rid 11166 ax-rnegex 11167 ax-rrecex 11168 ax-cnre 11169 ax-pre-lttri 11170 ax-pre-lttrn 11171 ax-pre-ltadd 11172 ax-pre-mulgt0 11173

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-card 9921 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244 df-le 11245 df-sub 11439 df-neg 11440 df-nn 12230 df-n0 12501 df-xnn0 12574 df-z 12588 df-uz 12859 df-rp 13013 df-fz 13532 df-fzo 13679 df-hash 14363 df-word 14547 df-lsw 14596 df-concat 14604 df-s1 14630 df-substr 14675 df-pfx 14705 df-chn 18658

This theorem is referenced by: (None)

W3C validator