| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqidd 2737 | . . . . 5
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → (♯‘𝐶) = (♯‘𝐶)) | 
| 2 |  | ischn 32997 | . . . . . . . 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 32919 | . . . 4
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → 𝐶:(0..^(♯‘𝐶))⟶𝐴) | 
| 7 | 6 | frnd 6743 | . . 3
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → ran 𝐶 ⊆ 𝐴) | 
| 8 |  | simpl 482 | . . 3
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → < Po 𝐴) | 
| 9 |  | poss 5593 | . . 3
⊢ (ran
𝐶 ⊆ 𝐴 → ( < Po 𝐴 → < Po ran 𝐶)) | 
| 10 | 7, 8, 9 | sylc 65 | . 2
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → < Po ran 𝐶) | 
| 11 |  | fzossz 13720 | . . . . . . . . 9
⊢
(0..^(♯‘𝐶)) ⊆ ℤ | 
| 12 |  | simp-4r 783 | . . . . . . . . 9
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ (0..^(♯‘𝐶))) | 
| 13 | 11, 12 | sselid 3980 | . . . . . . . 8
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ ℤ) | 
| 14 | 13 | zred 12724 | . . . . . . 7
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑖 ∈ ℝ) | 
| 15 |  | simplr 768 | . . . . . . . . 9
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ (0..^(♯‘𝐶))) | 
| 16 | 11, 15 | sselid 3980 | . . . . . . . 8
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ ℤ) | 
| 17 | 16 | zred 12724 | . . . . . . 7
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → 𝑗 ∈ ℝ) | 
| 18 | 14, 17 | lttri4d 11403 | . . . . . 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 13704 | . . . . . . . . . . . 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 13703 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (0..^𝑗) ↔ (𝑖 ∈ (ℤ≥‘0)
∧ 𝑗 ∈ ℤ
∧ 𝑖 < 𝑗)) | 
| 27 | 23, 24, 25, 26 | syl3anbrc 1343 | . . . . . . . . . 10
⊢ (((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑖 < 𝑗) → 𝑖 ∈ (0..^𝑗)) | 
| 28 | 19, 20, 21, 27 | chnlt 33004 | . . . . . . . . 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 5173 | . . . . . . . 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 6909 | . . . . . . . . 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 2784 | . . . . . . . 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 13704 | . . . . . . . . . . . 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 13703 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0..^𝑖) ↔ (𝑗 ∈ (ℤ≥‘0)
∧ 𝑖 ∈ ℤ
∧ 𝑗 < 𝑖)) | 
| 47 | 43, 44, 45, 46 | syl3anbrc 1343 | . . . . . . . . . 10
⊢ (((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑗 ∈ (0..^𝑖)) | 
| 48 | 39, 40, 41, 47 | chnlt 33004 | . . . . . . . . 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 5173 | . . . . . . . 8
⊢ (((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) ∧ 𝑗 < 𝑖) → 𝑦 < 𝑥) | 
| 52 | 51 | ex 412 | . . . . . . 7
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑗 < 𝑖 → 𝑦 < 𝑥)) | 
| 53 | 32, 38, 52 | 3orim123d 1445 | . . . . . 6
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → ((𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥))) | 
| 54 | 18, 53 | mpd 15 | . . . . 5
⊢ ((((((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) ∧ 𝑖 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑖) = 𝑥) ∧ 𝑗 ∈ (0..^(♯‘𝐶))) ∧ (𝐶‘𝑗) = 𝑦) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) | 
| 55 | 6 | ffnd 6736 | . . . . . . 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 6968 | . . . . . . 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 3161 | . . . 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 6968 | . . . . . 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 3161 | . . 3
⊢ ((((
< Po
𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ ran 𝐶) ∧ 𝑦 ∈ ran 𝐶) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) | 
| 68 | 67 | anasss 466 | . 2
⊢ ((( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) ∧ (𝑥 ∈ ran 𝐶 ∧ 𝑦 ∈ ran 𝐶)) → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥)) | 
| 69 | 10, 68 | issod 5626 | 1
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → < Or ran 𝐶) |