Step | Hyp | Ref
| Expression |
1 | | eldmg 5804 |
. . . 4
⊢ (𝐹 ∈ dom
⇝𝑟 → (𝐹 ∈ dom ⇝𝑟
↔ ∃𝑥 𝐹 ⇝𝑟
𝑥)) |
2 | 1 | ibi 266 |
. . 3
⊢ (𝐹 ∈ dom
⇝𝑟 → ∃𝑥 𝐹 ⇝𝑟 𝑥) |
3 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹 ⇝𝑟 𝑥) |
4 | | rlimrel 15183 |
. . . . . . . . . . . 12
⊢ Rel
⇝𝑟 |
5 | 4 | brrelex1i 5642 |
. . . . . . . . . . 11
⊢ (𝐹 ⇝𝑟
𝑥 → 𝐹 ∈ V) |
6 | 5 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹 ∈ V) |
7 | | vex 3434 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝑥 ∈ V) |
9 | | breldmg 5815 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ V ∧ 𝑥 ∈ V ∧ 𝐹 ⇝𝑟
𝑥) → 𝐹 ∈ dom ⇝𝑟
) |
10 | 6, 8, 3, 9 | syl3anc 1369 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹 ∈ dom ⇝𝑟
) |
11 | | breq2 5082 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (𝐹 ⇝𝑟 𝑦 ↔ 𝐹 ⇝𝑟 𝑥)) |
12 | 11 | biimprd 247 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 𝑦)) |
13 | 12 | spimevw 2001 |
. . . . . . . . . . 11
⊢ (𝐹 ⇝𝑟
𝑥 → ∃𝑦 𝐹 ⇝𝑟 𝑦) |
14 | 13 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → ∃𝑦 𝐹 ⇝𝑟 𝑦) |
15 | | rlimdmafv2.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹:𝐴⟶ℂ) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → 𝐹:𝐴⟶ℂ) |
18 | | rlimdmafv2.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → sup(𝐴, ℝ*, < ) =
+∞) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → sup(𝐴, ℝ*, < ) =
+∞) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → sup(𝐴, ℝ*, < ) =
+∞) |
21 | | simprl 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → 𝐹 ⇝𝑟 𝑦) |
22 | | simprr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → 𝐹 ⇝𝑟 𝑧) |
23 | 17, 20, 21, 22 | rlimuni 15240 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → 𝑦 = 𝑧) |
24 | 23 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → ((𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧) → 𝑦 = 𝑧)) |
25 | 24 | alrimivv 1934 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → ∀𝑦∀𝑧((𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧) → 𝑦 = 𝑧)) |
26 | | breq2 5082 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝐹 ⇝𝑟 𝑦 ↔ 𝐹 ⇝𝑟 𝑧)) |
27 | 26 | eu4 2618 |
. . . . . . . . . 10
⊢
(∃!𝑦 𝐹 ⇝𝑟
𝑦 ↔ (∃𝑦 𝐹 ⇝𝑟 𝑦 ∧ ∀𝑦∀𝑧((𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧) → 𝑦 = 𝑧))) |
28 | 14, 25, 27 | sylanbrc 582 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → ∃!𝑦 𝐹 ⇝𝑟 𝑦) |
29 | | dfdfat2 44571 |
. . . . . . . . 9
⊢ (
⇝𝑟 defAt 𝐹 ↔ (𝐹 ∈ dom ⇝𝑟
∧ ∃!𝑦 𝐹 ⇝𝑟
𝑦)) |
30 | 10, 28, 29 | sylanbrc 582 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) →
⇝𝑟 defAt 𝐹) |
31 | | dfatafv2iota 44653 |
. . . . . . . 8
⊢ (
⇝𝑟 defAt 𝐹 → ( ⇝𝑟
''''𝐹) =
(℩𝑤𝐹 ⇝𝑟 𝑤)) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (
⇝𝑟 ''''𝐹) = (℩𝑤𝐹 ⇝𝑟 𝑤)) |
33 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → 𝐹:𝐴⟶ℂ) |
34 | 18 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → sup(𝐴, ℝ*, < ) =
+∞) |
35 | | simprr 769 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → 𝐹 ⇝𝑟 𝑤) |
36 | | simprl 767 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → 𝐹 ⇝𝑟 𝑥) |
37 | 33, 34, 35, 36 | rlimuni 15240 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → 𝑤 = 𝑥) |
38 | 37 | expr 456 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (𝐹 ⇝𝑟 𝑤 → 𝑤 = 𝑥)) |
39 | | breq2 5082 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝐹 ⇝𝑟 𝑤 ↔ 𝐹 ⇝𝑟 𝑥)) |
40 | 3, 39 | syl5ibrcom 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (𝑤 = 𝑥 → 𝐹 ⇝𝑟 𝑤)) |
41 | 38, 40 | impbid 211 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (𝐹 ⇝𝑟 𝑤 ↔ 𝑤 = 𝑥)) |
42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ 𝑥 ∈ V) → (𝐹 ⇝𝑟 𝑤 ↔ 𝑤 = 𝑥)) |
43 | 42 | iota5 6413 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ 𝑥 ∈ V) → (℩𝑤𝐹 ⇝𝑟 𝑤) = 𝑥) |
44 | 43 | elvd 3437 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (℩𝑤𝐹 ⇝𝑟 𝑤) = 𝑥) |
45 | 32, 44 | eqtrd 2779 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (
⇝𝑟 ''''𝐹) = 𝑥) |
46 | 3, 45 | breqtrrd 5106 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹 ⇝𝑟 (
⇝𝑟 ''''𝐹)) |
47 | 46 | ex 412 |
. . . 4
⊢ (𝜑 → (𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 (
⇝𝑟 ''''𝐹))) |
48 | 47 | exlimdv 1939 |
. . 3
⊢ (𝜑 → (∃𝑥 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 (
⇝𝑟 ''''𝐹))) |
49 | 2, 48 | syl5 34 |
. 2
⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟
→ 𝐹
⇝𝑟 ( ⇝𝑟 ''''𝐹))) |
50 | 4 | releldmi 5854 |
. 2
⊢ (𝐹 ⇝𝑟 (
⇝𝑟 ''''𝐹) → 𝐹 ∈ dom ⇝𝑟
) |
51 | 49, 50 | impbid1 224 |
1
⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟
↔ 𝐹
⇝𝑟 ( ⇝𝑟 ''''𝐹))) |