| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eldmg 5909 | . . . 4
⊢ (𝐹 ∈ dom
⇝𝑟 → (𝐹 ∈ dom ⇝𝑟
↔ ∃𝑥 𝐹 ⇝𝑟
𝑥)) | 
| 2 | 1 | ibi 267 | . . 3
⊢ (𝐹 ∈ dom
⇝𝑟 → ∃𝑥 𝐹 ⇝𝑟 𝑥) | 
| 3 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹 ⇝𝑟 𝑥) | 
| 4 |  | rlimrel 15529 | . . . . . . . . . . . 12
⊢ Rel
⇝𝑟 | 
| 5 | 4 | brrelex1i 5741 | . . . . . . . . . . 11
⊢ (𝐹 ⇝𝑟
𝑥 → 𝐹 ∈ V) | 
| 6 | 5 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹 ∈ V) | 
| 7 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑥 ∈ V | 
| 8 | 7 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝑥 ∈ V) | 
| 9 |  | breldmg 5920 | . . . . . . . . . 10
⊢ ((𝐹 ∈ V ∧ 𝑥 ∈ V ∧ 𝐹 ⇝𝑟
𝑥) → 𝐹 ∈ dom ⇝𝑟
) | 
| 10 | 6, 8, 3, 9 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹 ∈ dom ⇝𝑟
) | 
| 11 |  | breq2 5147 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑥 → (𝐹 ⇝𝑟 𝑦 ↔ 𝐹 ⇝𝑟 𝑥)) | 
| 12 | 11 | biimprd 248 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 𝑦)) | 
| 13 | 12 | spimevw 1994 | . . . . . . . . . . 11
⊢ (𝐹 ⇝𝑟
𝑥 → ∃𝑦 𝐹 ⇝𝑟 𝑦) | 
| 14 | 13 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → ∃𝑦 𝐹 ⇝𝑟 𝑦) | 
| 15 |  | rlimdmafv.1 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹:𝐴⟶ℂ) | 
| 17 | 16 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → 𝐹:𝐴⟶ℂ) | 
| 18 |  | rlimdmafv.2 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → sup(𝐴, ℝ*, < ) =
+∞) | 
| 19 | 18 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → sup(𝐴, ℝ*, < ) =
+∞) | 
| 20 | 19 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → sup(𝐴, ℝ*, < ) =
+∞) | 
| 21 |  | simprl 771 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → 𝐹 ⇝𝑟 𝑦) | 
| 22 |  | simprr 773 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → 𝐹 ⇝𝑟 𝑧) | 
| 23 | 17, 20, 21, 22 | rlimuni 15586 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ (𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧)) → 𝑦 = 𝑧) | 
| 24 | 23 | ex 412 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → ((𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧) → 𝑦 = 𝑧)) | 
| 25 | 24 | alrimivv 1928 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → ∀𝑦∀𝑧((𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧) → 𝑦 = 𝑧)) | 
| 26 |  | breq2 5147 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝐹 ⇝𝑟 𝑦 ↔ 𝐹 ⇝𝑟 𝑧)) | 
| 27 | 26 | eu4 2615 | . . . . . . . . . 10
⊢
(∃!𝑦 𝐹 ⇝𝑟
𝑦 ↔ (∃𝑦 𝐹 ⇝𝑟 𝑦 ∧ ∀𝑦∀𝑧((𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧) → 𝑦 = 𝑧))) | 
| 28 | 14, 25, 27 | sylanbrc 583 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → ∃!𝑦 𝐹 ⇝𝑟 𝑦) | 
| 29 |  | dfdfat2 47140 | . . . . . . . . 9
⊢ (
⇝𝑟 defAt 𝐹 ↔ (𝐹 ∈ dom ⇝𝑟
∧ ∃!𝑦 𝐹 ⇝𝑟
𝑦)) | 
| 30 | 10, 28, 29 | sylanbrc 583 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) →
⇝𝑟 defAt 𝐹) | 
| 31 |  | afvfundmfveq 47150 | . . . . . . . 8
⊢ (
⇝𝑟 defAt 𝐹 → ( ⇝𝑟
'''𝐹) = (
⇝𝑟 ‘𝐹)) | 
| 32 | 30, 31 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (
⇝𝑟 '''𝐹) = ( ⇝𝑟
‘𝐹)) | 
| 33 |  | df-fv 6569 | . . . . . . . 8
⊢ (
⇝𝑟 ‘𝐹) = (℩𝑤𝐹 ⇝𝑟 𝑤) | 
| 34 | 15 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → 𝐹:𝐴⟶ℂ) | 
| 35 | 18 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → sup(𝐴, ℝ*, < ) =
+∞) | 
| 36 |  | simprr 773 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → 𝐹 ⇝𝑟 𝑤) | 
| 37 |  | simprl 771 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → 𝐹 ⇝𝑟 𝑥) | 
| 38 | 34, 35, 36, 37 | rlimuni 15586 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤)) → 𝑤 = 𝑥) | 
| 39 | 38 | expr 456 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (𝐹 ⇝𝑟 𝑤 → 𝑤 = 𝑥)) | 
| 40 |  | breq2 5147 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑥 → (𝐹 ⇝𝑟 𝑤 ↔ 𝐹 ⇝𝑟 𝑥)) | 
| 41 | 3, 40 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (𝑤 = 𝑥 → 𝐹 ⇝𝑟 𝑤)) | 
| 42 | 39, 41 | impbid 212 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (𝐹 ⇝𝑟 𝑤 ↔ 𝑤 = 𝑥)) | 
| 43 | 42 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ 𝑥 ∈ V) → (𝐹 ⇝𝑟 𝑤 ↔ 𝑤 = 𝑥)) | 
| 44 | 43 | iota5 6544 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) ∧ 𝑥 ∈ V) → (℩𝑤𝐹 ⇝𝑟 𝑤) = 𝑥) | 
| 45 | 44 | elvd 3486 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (℩𝑤𝐹 ⇝𝑟 𝑤) = 𝑥) | 
| 46 | 33, 45 | eqtrid 2789 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (
⇝𝑟 ‘𝐹) = 𝑥) | 
| 47 | 32, 46 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → (
⇝𝑟 '''𝐹) = 𝑥) | 
| 48 | 3, 47 | breqtrrd 5171 | . . . . 5
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝑥) → 𝐹 ⇝𝑟 (
⇝𝑟 '''𝐹)) | 
| 49 | 48 | ex 412 | . . . 4
⊢ (𝜑 → (𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 (
⇝𝑟 '''𝐹))) | 
| 50 | 49 | exlimdv 1933 | . . 3
⊢ (𝜑 → (∃𝑥 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 (
⇝𝑟 '''𝐹))) | 
| 51 | 2, 50 | syl5 34 | . 2
⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟
→ 𝐹
⇝𝑟 ( ⇝𝑟 '''𝐹))) | 
| 52 | 4 | releldmi 5959 | . 2
⊢ (𝐹 ⇝𝑟 (
⇝𝑟 '''𝐹) → 𝐹 ∈ dom ⇝𝑟
) | 
| 53 | 51, 52 | impbid1 225 | 1
⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟
↔ 𝐹
⇝𝑟 ( ⇝𝑟 '''𝐹))) |