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 18581

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 2740	. . . . 5 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → (♯‘𝐶) = (♯‘𝐶))
2		ischn 18564	. . . . . . 7 ⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
3	2	bilani 505	. . . . . 6 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
4	3	simpld 495	. . . . 5 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶 ∈ Word 𝐴)
5	1, 4	wrdfd 14472	. . . 4 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶:(0..^(♯‘𝐶))⟶𝐴)
6	5	frnd 6663	. . 3 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → ran 𝐶 ⊆ 𝐴)
7		simpl 483	. . 3 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Po 𝐴)
8		poss 5528	. . 3 ⊢ (ran 𝐶 ⊆ 𝐴 → ( < Po 𝐴 → < Po ran 𝐶))
9	6, 7, 8	sylc 65	. 2 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Po ran 𝐶)
10		fzossz 13625	. . . . . . . . 9 ⊢ (0..^(♯‘𝐶)) ⊆ ℤ
11		simp-4r 789	. . . . . . . . 9 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ (0..^(♯‘𝐶)))
12	10, 11	sselid 3913	. . . . . . . 8 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ ℤ)
13	12	zred 12624	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ ℝ)
14		simplr 774	. . . . . . . . 9 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ (0..^(♯‘𝐶)))
15	10, 14	sselid 3913	. . . . . . . 8 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ ℤ)
16	15	zred 12624	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ ℝ)
17	13, 16	lttri4d 11278	. . . . . 6 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖))
18		simp-8l 796	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → < Po 𝐴)
19		simp-8r 797	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝐶 ∈ ( < Chain 𝐴))
20		simpllr 781	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑗 ∈ (0..^(♯‘𝐶)))
21		elfzouz 13609	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0..^(♯‘𝐶)) → 𝑖 ∈ (ℤ_≥‘0))
22	21	ad5antlr 741	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 ∈ (ℤ_≥‘0))
23	15	adantr 481	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑗 ∈ ℤ)
24		simpr 485	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 < 𝑗)
25		elfzo2 13607	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0..^𝑗) ↔ (𝑖 ∈ (ℤ_≥‘0) ∧ 𝑗 ∈ ℤ ∧ 𝑖 < 𝑗))
26	22, 23, 24, 25	syl3anbrc 1350	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 ∈ (0..^𝑗))
27	18, 19, 20, 26	chnlt 18580	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑖) < (𝐶‘𝑗))
28		simp-4r 789	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑖) = 𝑥)
29		simplr 774	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → (𝐶‘𝑗) = 𝑦)
30	27, 28, 29	3brtr3d 5103	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑥 < 𝑦)
31	30	ex 413	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 < 𝑗 → 𝑥 < 𝑦))
32		simpr 485	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
33	32	fveq2d 6831	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑖) = (𝐶‘𝑗))
34		simp-4r 789	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑖) = 𝑥)
35		simplr 774	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → (𝐶‘𝑗) = 𝑦)
36	33, 34, 35	3eqtr3d 2782	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 = 𝑗) → 𝑥 = 𝑦)
37	36	ex 413	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑖 = 𝑗 → 𝑥 = 𝑦))
38		simp-8l 796	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → < Po 𝐴)
39		simp-8r 797	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝐶 ∈ ( < Chain 𝐴))
40	11	adantr 481	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑖 ∈ (0..^(♯‘𝐶)))
41		elfzouz 13609	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0..^(♯‘𝐶)) → 𝑗 ∈ (ℤ_≥‘0))
42	41	ad3antlr 737	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 ∈ (ℤ_≥‘0))
43	12	adantr 481	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑖 ∈ ℤ)
44		simpr 485	. . . . . . . . . . 11 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 < 𝑖)
45		elfzo2 13607	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0..^𝑖) ↔ (𝑗 ∈ (ℤ_≥‘0) ∧ 𝑖 ∈ ℤ ∧ 𝑗 < 𝑖))
46	42, 43, 44, 45	syl3anbrc 1350	. . . . . . . . . 10 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 ∈ (0..^𝑖))
47	38, 39, 40, 46	chnlt 18580	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑗) < (𝐶‘𝑖))
48		simplr 774	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑗) = 𝑦)
49		simp-4r 789	. . . . . . . . 9 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → (𝐶‘𝑖) = 𝑥)
50	47, 48, 49	3brtr3d 5103	. . . . . . . 8 ⊢ ((((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑦 < 𝑥)
51	50	ex 413	. . . . . . 7 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑗 < 𝑖 → 𝑦 < 𝑥))
52	31, 37, 51	3orim123d 1452	. . . . . 6 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → ((𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)))
53	17, 52	mpd 15	. . . . 5 ⊢ (((((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
54	5	ffnd 6656	. . . . . . 7 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → 𝐶 Fn (0..^(♯‘𝐶)))
55	54	ad4antr 738	. . . . . 6 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → 𝐶 Fn (0..^(♯‘𝐶)))
56		simpllr 781	. . . . . 6 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → 𝑦 ∈ ran 𝐶)
57		fvelrnb 6887	. . . . . . 7 ⊢ (𝐶 Fn (0..^(♯‘𝐶)) → (𝑦 ∈ ran 𝐶 ↔ ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦))
58	57	biimpa 477	. . . . . 6 ⊢ ((𝐶 Fn (0..^(♯‘𝐶)) ∧ 𝑦 ∈ ran 𝐶) → ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦)
59	55, 56, 58	syl2anc 590	. . . . 5 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → ∃𝑗 ∈ (0..^(♯‘𝐶))(𝐶‘𝑗) = 𝑦)
60	53, 59	r19.29a 3147	. . . 4 ⊢ (((((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
61	54	ad2antrr 732	. . . . 5 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → 𝐶 Fn (0..^(♯‘𝐶)))
62		simplr 774	. . . . 5 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → 𝑥 ∈ ran 𝐶)
63		fvelrnb 6887	. . . . . 6 ⊢ (𝐶 Fn (0..^(♯‘𝐶)) → (𝑥 ∈ ran 𝐶 ↔ ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥))
64	63	biimpa 477	. . . . 5 ⊢ ((𝐶 Fn (0..^(♯‘𝐶)) ∧ 𝑥 ∈ ran 𝐶) → ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥)
65	61, 62, 64	syl2anc 590	. . . 4 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → ∃𝑖 ∈ (0..^(♯‘𝐶))(𝐶‘𝑖) = 𝑥)
66	60, 65	r19.29a 3147	. . 3 ⊢ (((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
67	66	anasss 467	. 2 ⊢ ((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) ∧ (𝑥 ∈ ran 𝐶 ∧ 𝑦 ∈ ran 𝐶)) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))
68	9, 67	issod 5561	1 ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Or ran 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∨ w3o 1091 = wceq 1547 ∈ wcel 2119 ∀wral 3053 ∃wrex 3063 ∖ cdif 3880 ⊆ wss 3883 {csn 4555 class class class wbr 5072 Po wpo 5524 Or wor 5525 dom cdm 5618 ran crn 5619 Fn wfn 6480 ‘cfv 6485 (class class class)co 7356 0cc0 11029 1c1 11030 < clt 11170 − cmin 11368 ℤcz 12515 ℤ_≥cuz 12779 ..^cfzo 13599 ♯chash 14283 Word cword 14466 Chain cchn 18562

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-rp 12934 df-fz 13453 df-fzo 13600 df-hash 14284 df-word 14467 df-lsw 14516 df-concat 14524 df-s1 14550 df-substr 14595 df-pfx 14625 df-chn 18563

This theorem is referenced by: (None)

W3C validator