| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqidd |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → ( ♯ ‘ 𝐶 ) = ( ♯ ‘ 𝐶 ) ) |
| 2 |
|
ischn |
⊢ ( 𝐶 ∈ ( < Chain 𝐴 ) ↔ ( 𝐶 ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑛 − 1 ) ) < ( 𝐶 ‘ 𝑛 ) ) ) |
| 3 |
2
|
biimpi |
⊢ ( 𝐶 ∈ ( < Chain 𝐴 ) → ( 𝐶 ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑛 − 1 ) ) < ( 𝐶 ‘ 𝑛 ) ) ) |
| 4 |
3
|
adantl |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → ( 𝐶 ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom 𝐶 ∖ { 0 } ) ( 𝐶 ‘ ( 𝑛 − 1 ) ) < ( 𝐶 ‘ 𝑛 ) ) ) |
| 5 |
4
|
simpld |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → 𝐶 ∈ Word 𝐴 ) |
| 6 |
1 5
|
wrdfd |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → 𝐶 : ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 ) |
| 7 |
6
|
frnd |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → ran 𝐶 ⊆ 𝐴 ) |
| 8 |
|
simpl |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → < Po 𝐴 ) |
| 9 |
|
poss |
⊢ ( ran 𝐶 ⊆ 𝐴 → ( < Po 𝐴 → < Po ran 𝐶 ) ) |
| 10 |
7 8 9
|
sylc |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → < Po ran 𝐶 ) |
| 11 |
|
fzossz |
⊢ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ⊆ ℤ |
| 12 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) |
| 13 |
11 12
|
sselid |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → 𝑖 ∈ ℤ ) |
| 14 |
13
|
zred |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → 𝑖 ∈ ℝ ) |
| 15 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) |
| 16 |
11 15
|
sselid |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → 𝑗 ∈ ℤ ) |
| 17 |
16
|
zred |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → 𝑗 ∈ ℝ ) |
| 18 |
14 17
|
lttri4d |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → ( 𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖 ) ) |
| 19 |
|
simp-8l |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → < Po 𝐴 ) |
| 20 |
|
simp-8r |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → 𝐶 ∈ ( < Chain 𝐴 ) ) |
| 21 |
|
simpllr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) |
| 22 |
|
elfzouz |
⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) ) |
| 23 |
22
|
ad5antlr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) ) |
| 24 |
16
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → 𝑗 ∈ ℤ ) |
| 25 |
|
simpr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → 𝑖 < 𝑗 ) |
| 26 |
|
elfzo2 |
⊢ ( 𝑖 ∈ ( 0 ..^ 𝑗 ) ↔ ( 𝑖 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑗 ∈ ℤ ∧ 𝑖 < 𝑗 ) ) |
| 27 |
23 24 25 26
|
syl3anbrc |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → 𝑖 ∈ ( 0 ..^ 𝑗 ) ) |
| 28 |
19 20 21 27
|
chnlt |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → ( 𝐶 ‘ 𝑖 ) < ( 𝐶 ‘ 𝑗 ) ) |
| 29 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → ( 𝐶 ‘ 𝑖 ) = 𝑥 ) |
| 30 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → ( 𝐶 ‘ 𝑗 ) = 𝑦 ) |
| 31 |
28 29 30
|
3brtr3d |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 < 𝑗 ) → 𝑥 < 𝑦 ) |
| 32 |
31
|
ex |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → ( 𝑖 < 𝑗 → 𝑥 < 𝑦 ) ) |
| 33 |
|
simpr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 = 𝑗 ) → 𝑖 = 𝑗 ) |
| 34 |
33
|
fveq2d |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 = 𝑗 ) → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑗 ) ) |
| 35 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 = 𝑗 ) → ( 𝐶 ‘ 𝑖 ) = 𝑥 ) |
| 36 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 = 𝑗 ) → ( 𝐶 ‘ 𝑗 ) = 𝑦 ) |
| 37 |
34 35 36
|
3eqtr3d |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑖 = 𝑗 ) → 𝑥 = 𝑦 ) |
| 38 |
37
|
ex |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → ( 𝑖 = 𝑗 → 𝑥 = 𝑦 ) ) |
| 39 |
|
simp-8l |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → < Po 𝐴 ) |
| 40 |
|
simp-8r |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → 𝐶 ∈ ( < Chain 𝐴 ) ) |
| 41 |
12
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) |
| 42 |
|
elfzouz |
⊢ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 0 ) ) |
| 43 |
42
|
ad3antlr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → 𝑗 ∈ ( ℤ≥ ‘ 0 ) ) |
| 44 |
13
|
adantr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → 𝑖 ∈ ℤ ) |
| 45 |
|
simpr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → 𝑗 < 𝑖 ) |
| 46 |
|
elfzo2 |
⊢ ( 𝑗 ∈ ( 0 ..^ 𝑖 ) ↔ ( 𝑗 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑖 ∈ ℤ ∧ 𝑗 < 𝑖 ) ) |
| 47 |
43 44 45 46
|
syl3anbrc |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → 𝑗 ∈ ( 0 ..^ 𝑖 ) ) |
| 48 |
39 40 41 47
|
chnlt |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → ( 𝐶 ‘ 𝑗 ) < ( 𝐶 ‘ 𝑖 ) ) |
| 49 |
|
simplr |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → ( 𝐶 ‘ 𝑗 ) = 𝑦 ) |
| 50 |
|
simp-4r |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → ( 𝐶 ‘ 𝑖 ) = 𝑥 ) |
| 51 |
48 49 50
|
3brtr3d |
⊢ ( ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ∧ 𝑗 < 𝑖 ) → 𝑦 < 𝑥 ) |
| 52 |
51
|
ex |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → ( 𝑗 < 𝑖 → 𝑦 < 𝑥 ) ) |
| 53 |
32 38 52
|
3orim123d |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → ( ( 𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖 ) → ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) ) ) |
| 54 |
18 53
|
mpd |
⊢ ( ( ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑗 ) = 𝑦 ) → ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) ) |
| 55 |
6
|
ffnd |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) |
| 56 |
55
|
ad4antr |
⊢ ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) → 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) |
| 57 |
|
simpllr |
⊢ ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) → 𝑦 ∈ ran 𝐶 ) |
| 58 |
|
fvelrnb |
⊢ ( 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → ( 𝑦 ∈ ran 𝐶 ↔ ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑗 ) = 𝑦 ) ) |
| 59 |
58
|
biimpa |
⊢ ( ( 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ∧ 𝑦 ∈ ran 𝐶 ) → ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑗 ) = 𝑦 ) |
| 60 |
56 57 59
|
syl2anc |
⊢ ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) → ∃ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑗 ) = 𝑦 ) |
| 61 |
54 60
|
r19.29a |
⊢ ( ( ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = 𝑥 ) → ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) ) |
| 62 |
55
|
ad2antrr |
⊢ ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) → 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ) |
| 63 |
|
simplr |
⊢ ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) → 𝑥 ∈ ran 𝐶 ) |
| 64 |
|
fvelrnb |
⊢ ( 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → ( 𝑥 ∈ ran 𝐶 ↔ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑖 ) = 𝑥 ) ) |
| 65 |
64
|
biimpa |
⊢ ( ( 𝐶 Fn ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ∧ 𝑥 ∈ ran 𝐶 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑖 ) = 𝑥 ) |
| 66 |
62 63 65
|
syl2anc |
⊢ ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) → ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) ( 𝐶 ‘ 𝑖 ) = 𝑥 ) |
| 67 |
61 66
|
r19.29a |
⊢ ( ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ 𝑥 ∈ ran 𝐶 ) ∧ 𝑦 ∈ ran 𝐶 ) → ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) ) |
| 68 |
67
|
anasss |
⊢ ( ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) ∧ ( 𝑥 ∈ ran 𝐶 ∧ 𝑦 ∈ ran 𝐶 ) ) → ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥 ) ) |
| 69 |
10 68
|
issod |
⊢ ( ( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴 ) ) → < Or ran 𝐶 ) |