Proof of Theorem iscauf
| Step | Hyp | Ref
| Expression |
| 1 | | iscau3.3 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
| 2 | | elfvdm 6943 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 ∈ dom ∞Met) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ dom ∞Met) |
| 4 | | cnex 11236 |
. . . . 5
⊢ ℂ
∈ V |
| 5 | 3, 4 | jctir 520 |
. . . 4
⊢ (𝜑 → (𝑋 ∈ dom ∞Met ∧ ℂ ∈
V)) |
| 6 | | iscauf.7 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶𝑋) |
| 7 | | iscau3.2 |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 8 | | uzssz 12899 |
. . . . . . 7
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
| 9 | | zsscn 12621 |
. . . . . . 7
⊢ ℤ
⊆ ℂ |
| 10 | 8, 9 | sstri 3993 |
. . . . . 6
⊢
(ℤ≥‘𝑀) ⊆ ℂ |
| 11 | 7, 10 | eqsstri 4030 |
. . . . 5
⊢ 𝑍 ⊆
ℂ |
| 12 | 6, 11 | jctir 520 |
. . . 4
⊢ (𝜑 → (𝐹:𝑍⟶𝑋 ∧ 𝑍 ⊆ ℂ)) |
| 13 | | elpm2r 8885 |
. . . 4
⊢ (((𝑋 ∈ dom ∞Met ∧
ℂ ∈ V) ∧ (𝐹:𝑍⟶𝑋 ∧ 𝑍 ⊆ ℂ)) → 𝐹 ∈ (𝑋 ↑pm
ℂ)) |
| 14 | 5, 12, 13 | syl2anc 584 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm
ℂ)) |
| 15 | 14 | biantrurd 532 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥)))) |
| 16 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝐷 ∈ (∞Met‘𝑋)) |
| 17 | | iscau4.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = 𝐵) |
| 18 | 17 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑗) = 𝐵) |
| 19 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝐹:𝑍⟶𝑋) |
| 20 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑗 ∈ 𝑍) |
| 21 | 19, 20 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑗) ∈ 𝑋) |
| 22 | 18, 21 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝐵 ∈ 𝑋) |
| 23 | 7 | uztrn2 12897 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 24 | | iscau4.5 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) |
| 25 | 23, 24 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) = 𝐴) |
| 26 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑍⟶𝑋 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑋) |
| 27 | 6, 23, 26 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ∈ 𝑋) |
| 28 | 25, 27 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝐴 ∈ 𝑋) |
| 29 | | xmetsym 24357 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵)) |
| 30 | 16, 22, 28, 29 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵)) |
| 31 | 30 | breq1d 5153 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐵𝐷𝐴) < 𝑥 ↔ (𝐴𝐷𝐵) < 𝑥)) |
| 32 | | fdm 6745 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑍⟶𝑋 → dom 𝐹 = 𝑍) |
| 33 | 32 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑍⟶𝑋 → (𝑘 ∈ dom 𝐹 ↔ 𝑘 ∈ 𝑍)) |
| 34 | 33 | biimpar 477 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑍⟶𝑋 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ dom 𝐹) |
| 35 | 6, 23, 34 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → 𝑘 ∈ dom 𝐹) |
| 36 | 35, 28 | jca 511 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋)) |
| 37 | 36 | biantrurd 532 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐴𝐷𝐵) < 𝑥 ↔ ((𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋) ∧ (𝐴𝐷𝐵) < 𝑥))) |
| 38 | | df-3an 1089 |
. . . . . . . 8
⊢ ((𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋) ∧ (𝐴𝐷𝐵) < 𝑥)) |
| 39 | 37, 38 | bitr4di 289 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐴𝐷𝐵) < 𝑥 ↔ (𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥))) |
| 40 | 31, 39 | bitrd 279 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((𝐵𝐷𝐴) < 𝑥 ↔ (𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥))) |
| 41 | 40 | anassrs 467 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐵𝐷𝐴) < 𝑥 ↔ (𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥))) |
| 42 | 41 | ralbidva 3176 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵𝐷𝐴) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥))) |
| 43 | 42 | rexbidva 3177 |
. . 3
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵𝐷𝐴) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥))) |
| 44 | 43 | ralbidv 3178 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵𝐷𝐴) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥))) |
| 45 | | iscau3.4 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 46 | 7, 1, 45, 24, 17 | iscau4 25313 |
. 2
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥)))) |
| 47 | 15, 44, 46 | 3bitr4rd 312 |
1
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵𝐷𝐴) < 𝑥)) |