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 18530

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 2732	. . . . 5 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → (♯‘𝐶) = (♯‘𝐶))
2		ischn 18513	. . . . . . . 8 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
3	2	biimpi 216	. . . . . . 7 ⊢ (𝐶 ∈ ( < Chain 𝐴) → (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
4	3	adantl 481	. . . . . 6 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
5	4	simpld 494	. . . . 5 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶 ∈ Word 𝐴)
6	1, 5	wrdfd 14426	. . . 4 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶:(0..^(♯‘𝐶))⟶𝐴)
7	6	frnd 6659	. . 3 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → ran 𝐶 ⊆ 𝐴)
8		simpl 482	. . 3 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Po 𝐴)
9		poss 5526	. . 3 ⊢ (ran 𝐶 ⊆ 𝐴 → ( < Po 𝐴 → < Po ran 𝐶))
10	7, 8, 9	sylc 65	. 2 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Po ran 𝐶)
11		fzossz 13579	. . . . . . . . 9 ⊢ (0..^(♯‘𝐶)) ⊆ ℤ
12		simp-4r 783	. . . . . . . . 9 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ (0..^(♯‘𝐶)))
13	11, 12	sselid 3932	. . . . . . . 8 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ ℤ)
14	13	zred 12577	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ ℝ)
15		simplr 768	. . . . . . . . 9 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ (0..^(♯‘𝐶)))
16	11, 15	sselid 3932	. . . . . . . 8 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ ℤ)
17	16	zred 12577	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ ℝ)
18	14, 17	lttri4d 11254	. . . . . 6 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖))
19		simp-8l 790	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → < Po 𝐴)
20		simp-8r 791	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝐶 ∈ ( < Chain 𝐴))
21		simpllr 775	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (0..^(♯‘𝐶)))
22		elfzouz 13563	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0..^(♯‘𝐶)) → 𝑖 ∈ (ℤ_≥‘0))
23	22	ad5antlr 735	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 ∈ (ℤ_≥‘0))
24	16	adantr 480	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
25		simpr 484	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
26		elfzo2 13562	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0..^𝑗) ↔ (𝑖 ∈ (ℤ_≥‘0) ∧ 𝑗 ∈ ℤ ∧ 𝑖 < 𝑗))
27	23, 24, 25, 26	syl3anbrc 1344	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 ∈ (0..^𝑗))
28	19, 20, 21, 27	chnlt 18529	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑖) < (𝐶‘𝑗))
29		simp-4r 783	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑖) = 𝑥)
30		simplr 768	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑗) = 𝑦)
31	28, 29, 30	3brtr3d 5122	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑥 < 𝑦)
32	31	ex 412	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 < 𝑗 → 𝑥 < 𝑦))
33		simpr 484	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
34	33	fveq2d 6826	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑖) = (𝐶‘𝑗))
35		simp-4r 783	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑖) = 𝑥)
36		simplr 768	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑗) = 𝑦)
37	34, 35, 36	3eqtr3d 2774	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → 𝑥 = 𝑦)
38	37	ex 412	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 = 𝑗 → 𝑥 = 𝑦))
39		simp-8l 790	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → < Po 𝐴)
40		simp-8r 791	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝐶 ∈ ( < Chain 𝐴))
41	12	adantr 480	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑖 ∈ (0..^(♯‘𝐶)))
42		elfzouz 13563	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0..^(♯‘𝐶)) → 𝑗 ∈ (ℤ_≥‘0))
43	42	ad3antlr 731	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 ∈ (ℤ_≥‘0))
44	13	adantr 480	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑖 ∈ ℤ)
45		simpr 484	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 < 𝑖)
46		elfzo2 13562	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑖) ↔ (𝑗 ∈ (ℤ_≥‘0) ∧ 𝑖 ∈ ℤ ∧ 𝑗 < 𝑖))
47	43, 44, 45, 46	syl3anbrc 1344	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 ∈ (0..^𝑖))
48	39, 40, 41, 47	chnlt 18529	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑗) < (𝐶‘𝑖))
49		simplr 768	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑗) = 𝑦)
50		simp-4r 783	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑖) = 𝑥)
51	48, 49, 50	3brtr3d 5122	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑦 < 𝑥)
52	51	ex 412	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑗 < 𝑖 → 𝑦 < 𝑥))
53	32, 38, 52	3orim123d 1446	. . . . . 6 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → ((𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)))
54	18, 53	mpd 15	. . . . 5 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
55	6	ffnd 6652	. . . . . . 7 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶 Fn (0..^(♯‘𝐶)))
56	55	ad4antr 732	. . . . . 6 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → 𝐶 Fn (0..^(♯‘𝐶)))
57		simpllr 775	. . . . . 6 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → 𝑦 ∈ ran 𝐶)
58		fvelrnb 6882	. . . . . . 7 ⊢ (𝐶 Fn (0..^(♯‘𝐶)) → (𝑦 ∈ ran 𝐶 ↔ ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦))
59	58	biimpa 476	. . . . . 6 ⊢ ((𝐶 Fn (0..^(♯‘𝐶)) ∧ 𝑦 ∈ ran 𝐶) → ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦)
60	56, 57, 59	syl2anc 584	. . . . 5 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦)
61	54, 60	r19.29a 3140	. . . 4 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
62	55	ad2antrr 726	. . . . 5 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → 𝐶 Fn (0..^(♯‘𝐶)))
63		simplr 768	. . . . 5 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → 𝑥 ∈ ran 𝐶)
64		fvelrnb 6882	. . . . . 6 ⊢ (𝐶 Fn (0..^(♯‘𝐶)) → (𝑥 ∈ ran 𝐶 ↔ ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥))
65	64	biimpa 476	. . . . 5 ⊢ ((𝐶 Fn (0..^(♯‘𝐶)) ∧ 𝑥 ∈ ran 𝐶) → ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥)
66	62, 63, 65	syl2anc 584	. . . 4 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥)
67	61, 66	r19.29a 3140	. . 3 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
68	67	anasss 466	. 2 ⊢ ((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ (𝑥 ∈ ran 𝐶 ∧ 𝑦 ∈ ran 𝐶)) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
69	10, 68	issod 5559	1 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Or ran 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1085 = wceq 1541 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 ∖ cdif 3899 ⊆ wss 3902 {csn 4576 class class class wbr 5091 Po wpo 5522 Or wor 5523 dom cdm 5616 ran crn 5617 Fn wfn 6476 ‘cfv 6481 (class class class)co 7346 0cc0 11006 1c1 11007 < clt 11146 − cmin 11344 ℤcz 12468 ℤ_≥cuz 12732 ..^cfzo 13554 ♯chash 14237 Word cword 14420 Chain cchn 18511

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-n0 12382 df-xnn0 12455 df-z 12469 df-uz 12733 df-rp 12891 df-fz 13408 df-fzo 13555 df-hash 14238 df-word 14421 df-lsw 14470 df-concat 14478 df-s1 14504 df-substr 14549 df-pfx 14579 df-chn 18512

This theorem is referenced by: (None)

W3C validator