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