Proof of Theorem erdszelem4
| Step | Hyp | Ref
| Expression |
| 1 | | elfznn 13593 |
. . . . 5
⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ) |
| 2 | 1 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → 𝐴 ∈ ℕ) |
| 3 | | elfz1end 13594 |
. . . 4
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ (1...𝐴)) |
| 4 | 2, 3 | sylib 218 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → 𝐴 ∈ (1...𝐴)) |
| 5 | 4 | snssd 4809 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → {𝐴} ⊆ (1...𝐴)) |
| 6 | | elsni 4643 |
. . . . . . 7
⊢ (𝑥 ∈ {𝐴} → 𝑥 = 𝐴) |
| 7 | | elsni 4643 |
. . . . . . 7
⊢ (𝑦 ∈ {𝐴} → 𝑦 = 𝐴) |
| 8 | 6, 7 | breqan12d 5159 |
. . . . . 6
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴}) → (𝑥 < 𝑦 ↔ 𝐴 < 𝐴)) |
| 9 | 8 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (1...𝑁)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) → (𝑥 < 𝑦 ↔ 𝐴 < 𝐴)) |
| 10 | | fzssuz 13605 |
. . . . . . . . 9
⊢
(1...𝑁) ⊆
(ℤ≥‘1) |
| 11 | | uzssz 12899 |
. . . . . . . . . 10
⊢
(ℤ≥‘1) ⊆ ℤ |
| 12 | | zssre 12620 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℝ |
| 13 | 11, 12 | sstri 3993 |
. . . . . . . . 9
⊢
(ℤ≥‘1) ⊆ ℝ |
| 14 | 10, 13 | sstri 3993 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℝ |
| 15 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → 𝐴 ∈ (1...𝑁)) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ (1...𝑁)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) → 𝐴 ∈ (1...𝑁)) |
| 17 | 14, 16 | sselid 3981 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ (1...𝑁)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) → 𝐴 ∈ ℝ) |
| 18 | 17 | ltnrd 11395 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ (1...𝑁)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) → ¬ 𝐴 < 𝐴) |
| 19 | 18 | pm2.21d 121 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ (1...𝑁)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) → (𝐴 < 𝐴 → (𝐹‘𝑥)𝑂(𝐹‘𝑦))) |
| 20 | 9, 19 | sylbid 240 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ (1...𝑁)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴})) → (𝑥 < 𝑦 → (𝐹‘𝑥)𝑂(𝐹‘𝑦))) |
| 21 | 20 | ralrimivva 3202 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} (𝑥 < 𝑦 → (𝐹‘𝑥)𝑂(𝐹‘𝑦))) |
| 22 | | erdsze.f |
. . . . . 6
⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ) |
| 23 | | f1f 6804 |
. . . . . 6
⊢ (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ) |
| 24 | 22, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:(1...𝑁)⟶ℝ) |
| 25 | 24 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → 𝐹:(1...𝑁)⟶ℝ) |
| 26 | 15 | snssd 4809 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → {𝐴} ⊆ (1...𝑁)) |
| 27 | | ltso 11341 |
. . . . . 6
⊢ < Or
ℝ |
| 28 | | soss 5612 |
. . . . . 6
⊢
((1...𝑁) ⊆
ℝ → ( < Or ℝ → < Or (1...𝑁))) |
| 29 | 14, 27, 28 | mp2 9 |
. . . . 5
⊢ < Or
(1...𝑁) |
| 30 | | erdszelem.o |
. . . . 5
⊢ 𝑂 Or ℝ |
| 31 | | soisores 7347 |
. . . . 5
⊢ ((( <
Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ {𝐴} ⊆ (1...𝑁))) → ((𝐹 ↾ {𝐴}) Isom < , 𝑂 ({𝐴}, (𝐹 “ {𝐴})) ↔ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} (𝑥 < 𝑦 → (𝐹‘𝑥)𝑂(𝐹‘𝑦)))) |
| 32 | 29, 30, 31 | mpanl12 702 |
. . . 4
⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ {𝐴} ⊆ (1...𝑁)) → ((𝐹 ↾ {𝐴}) Isom < , 𝑂 ({𝐴}, (𝐹 “ {𝐴})) ↔ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} (𝑥 < 𝑦 → (𝐹‘𝑥)𝑂(𝐹‘𝑦)))) |
| 33 | 25, 26, 32 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → ((𝐹 ↾ {𝐴}) Isom < , 𝑂 ({𝐴}, (𝐹 “ {𝐴})) ↔ ∀𝑥 ∈ {𝐴}∀𝑦 ∈ {𝐴} (𝑥 < 𝑦 → (𝐹‘𝑥)𝑂(𝐹‘𝑦)))) |
| 34 | 21, 33 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐹 ↾ {𝐴}) Isom < , 𝑂 ({𝐴}, (𝐹 “ {𝐴}))) |
| 35 | | snidg 4660 |
. . 3
⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ {𝐴}) |
| 36 | 35 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → 𝐴 ∈ {𝐴}) |
| 37 | | eqid 2737 |
. . 3
⊢ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} |
| 38 | 37 | erdszelem1 35196 |
. 2
⊢ ({𝐴} ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} ↔ ({𝐴} ⊆ (1...𝐴) ∧ (𝐹 ↾ {𝐴}) Isom < , 𝑂 ({𝐴}, (𝐹 “ {𝐴})) ∧ 𝐴 ∈ {𝐴})) |
| 39 | 5, 34, 36, 38 | syl3anbrc 1344 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → {𝐴} ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) |