MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvcnvrelem1 Structured version   Visualization version   GIF version

Theorem dvcnvrelem1 25287
Description: Lemma for dvcnvre 25289. (Contributed by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
dvcnvre.f (𝜑𝐹 ∈ (𝑋cn→ℝ))
dvcnvre.d (𝜑 → dom (ℝ D 𝐹) = 𝑋)
dvcnvre.z (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))
dvcnvre.1 (𝜑𝐹:𝑋1-1-onto𝑌)
dvcnvre.c (𝜑𝐶𝑋)
dvcnvre.r (𝜑𝑅 ∈ ℝ+)
dvcnvre.s (𝜑 → ((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋)
Assertion
Ref Expression
dvcnvrelem1 (𝜑 → (𝐹𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))))

Proof of Theorem dvcnvrelem1
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvcnvre.d . . . . . 6 (𝜑 → dom (ℝ D 𝐹) = 𝑋)
2 dvbsss 25172 . . . . . 6 dom (ℝ D 𝐹) ⊆ ℝ
31, 2eqsstrrdi 3991 . . . . 5 (𝜑𝑋 ⊆ ℝ)
4 dvcnvre.c . . . . 5 (𝜑𝐶𝑋)
53, 4sseldd 3937 . . . 4 (𝜑𝐶 ∈ ℝ)
6 dvcnvre.r . . . . 5 (𝜑𝑅 ∈ ℝ+)
76rpred 12878 . . . 4 (𝜑𝑅 ∈ ℝ)
85, 7resubcld 11509 . . 3 (𝜑 → (𝐶𝑅) ∈ ℝ)
95, 7readdcld 11110 . . 3 (𝜑 → (𝐶 + 𝑅) ∈ ℝ)
105, 6ltsubrpd 12910 . . . . 5 (𝜑 → (𝐶𝑅) < 𝐶)
115, 6ltaddrpd 12911 . . . . 5 (𝜑𝐶 < (𝐶 + 𝑅))
128, 5, 9, 10, 11lttrd 11242 . . . 4 (𝜑 → (𝐶𝑅) < (𝐶 + 𝑅))
138, 9, 12ltled 11229 . . 3 (𝜑 → (𝐶𝑅) ≤ (𝐶 + 𝑅))
14 dvcnvre.s . . . 4 (𝜑 → ((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋)
15 dvcnvre.f . . . 4 (𝜑𝐹 ∈ (𝑋cn→ℝ))
16 rescncf 24166 . . . 4 (((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋 → (𝐹 ∈ (𝑋cn→ℝ) → (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶𝑅)[,](𝐶 + 𝑅))–cn→ℝ)))
1714, 15, 16sylc 65 . . 3 (𝜑 → (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) ∈ (((𝐶𝑅)[,](𝐶 + 𝑅))–cn→ℝ))
188, 9, 13, 17evthicc2 24730 . 2 (𝜑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))
19 cncff 24162 . . . . . . . . 9 (𝐹 ∈ (𝑋cn→ℝ) → 𝐹:𝑋⟶ℝ)
2015, 19syl 17 . . . . . . . 8 (𝜑𝐹:𝑋⟶ℝ)
2120, 4ffvelcdmd 7023 . . . . . . 7 (𝜑 → (𝐹𝐶) ∈ ℝ)
2221adantr 482 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹𝐶) ∈ ℝ)
238rexrd 11131 . . . . . . . . . . . 12 (𝜑 → (𝐶𝑅) ∈ ℝ*)
249rexrd 11131 . . . . . . . . . . . 12 (𝜑 → (𝐶 + 𝑅) ∈ ℝ*)
25 lbicc2 13302 . . . . . . . . . . . 12 (((𝐶𝑅) ∈ ℝ* ∧ (𝐶 + 𝑅) ∈ ℝ* ∧ (𝐶𝑅) ≤ (𝐶 + 𝑅)) → (𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))
2623, 24, 13, 25syl3anc 1371 . . . . . . . . . . 11 (𝜑 → (𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))
2726adantr 482 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))
288, 5, 10ltled 11229 . . . . . . . . . . . 12 (𝜑 → (𝐶𝑅) ≤ 𝐶)
295, 9, 11ltled 11229 . . . . . . . . . . . 12 (𝜑𝐶 ≤ (𝐶 + 𝑅))
30 elicc2 13250 . . . . . . . . . . . . 13 (((𝐶𝑅) ∈ ℝ ∧ (𝐶 + 𝑅) ∈ ℝ) → (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ↔ (𝐶 ∈ ℝ ∧ (𝐶𝑅) ≤ 𝐶𝐶 ≤ (𝐶 + 𝑅))))
318, 9, 30syl2anc 585 . . . . . . . . . . . 12 (𝜑 → (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ↔ (𝐶 ∈ ℝ ∧ (𝐶𝑅) ≤ 𝐶𝐶 ≤ (𝐶 + 𝑅))))
325, 28, 29, 31mpbir3and 1342 . . . . . . . . . . 11 (𝜑𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))
3332adantr 482 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))
3410adantr 482 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐶𝑅) < 𝐶)
35 isorel 7258 . . . . . . . . . . . . 13 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∧ ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ∧ 𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐶𝑅) < 𝐶 ↔ ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))
3635biimpd 228 . . . . . . . . . . . 12 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∧ ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ∧ 𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐶𝑅) < 𝐶 → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))
3736exp32 422 . . . . . . . . . . 11 ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → ((𝐶𝑅) < 𝐶 → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))))
3837com4l 92 . . . . . . . . . 10 ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → ((𝐶𝑅) < 𝐶 → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))))
3927, 33, 34, 38syl3c 66 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))
4027fvresd 6850 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) = (𝐹‘(𝐶𝑅)))
4133fvresd 6850 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) = (𝐹𝐶))
4240, 41breq12d 5110 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) ↔ (𝐹‘(𝐶𝑅)) < (𝐹𝐶)))
4339, 42sylibd 238 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐹‘(𝐶𝑅)) < (𝐹𝐶)))
4420adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝐹:𝑋⟶ℝ)
4544ffund 6660 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → Fun 𝐹)
4614adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ 𝑋)
4744fdmd 6667 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → dom 𝐹 = 𝑋)
4846, 47sseqtrrd 3977 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹)
49 funfvima2 7168 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ ((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹) → ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐹‘(𝐶𝑅)) ∈ (𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))))
5045, 48, 49syl2anc 585 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐹‘(𝐶𝑅)) ∈ (𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))))
5127, 50mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹‘(𝐶𝑅)) ∈ (𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅))))
52 df-ima 5638 . . . . . . . . . . . . 13 (𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅))) = ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))
53 simprr 771 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))
5452, 53eqtrid 2789 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))
5551, 54eleqtrd 2840 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹‘(𝐶𝑅)) ∈ (𝑥[,]𝑦))
56 elicc2 13250 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝐹‘(𝐶𝑅)) ∈ (𝑥[,]𝑦) ↔ ((𝐹‘(𝐶𝑅)) ∈ ℝ ∧ 𝑥 ≤ (𝐹‘(𝐶𝑅)) ∧ (𝐹‘(𝐶𝑅)) ≤ 𝑦)))
5756ad2antrl 726 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹‘(𝐶𝑅)) ∈ (𝑥[,]𝑦) ↔ ((𝐹‘(𝐶𝑅)) ∈ ℝ ∧ 𝑥 ≤ (𝐹‘(𝐶𝑅)) ∧ (𝐹‘(𝐶𝑅)) ≤ 𝑦)))
5855, 57mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹‘(𝐶𝑅)) ∈ ℝ ∧ 𝑥 ≤ (𝐹‘(𝐶𝑅)) ∧ (𝐹‘(𝐶𝑅)) ≤ 𝑦))
5958simp2d 1143 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝑥 ≤ (𝐹‘(𝐶𝑅)))
60 simprll 777 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝑥 ∈ ℝ)
6114, 26sseldd 3937 . . . . . . . . . . . 12 (𝜑 → (𝐶𝑅) ∈ 𝑋)
6220, 61ffvelcdmd 7023 . . . . . . . . . . 11 (𝜑 → (𝐹‘(𝐶𝑅)) ∈ ℝ)
6362adantr 482 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹‘(𝐶𝑅)) ∈ ℝ)
64 lelttr 11171 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ (𝐹‘(𝐶𝑅)) ∈ ℝ ∧ (𝐹𝐶) ∈ ℝ) → ((𝑥 ≤ (𝐹‘(𝐶𝑅)) ∧ (𝐹‘(𝐶𝑅)) < (𝐹𝐶)) → 𝑥 < (𝐹𝐶)))
6560, 63, 22, 64syl3anc 1371 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝑥 ≤ (𝐹‘(𝐶𝑅)) ∧ (𝐹‘(𝐶𝑅)) < (𝐹𝐶)) → 𝑥 < (𝐹𝐶)))
6659, 65mpand 693 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹‘(𝐶𝑅)) < (𝐹𝐶) → 𝑥 < (𝐹𝐶)))
6743, 66syld 47 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → 𝑥 < (𝐹𝐶)))
68 ubicc2 13303 . . . . . . . . . . . 12 (((𝐶𝑅) ∈ ℝ* ∧ (𝐶 + 𝑅) ∈ ℝ* ∧ (𝐶𝑅) ≤ (𝐶 + 𝑅)) → (𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))
6923, 24, 13, 68syl3anc 1371 . . . . . . . . . . 11 (𝜑 → (𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))
7069adantr 482 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))
7111adantr 482 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝐶 < (𝐶 + 𝑅))
72 isorel 7258 . . . . . . . . . . . . 13 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∧ (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ∧ (𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐶 < (𝐶 + 𝑅) ↔ ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))
7372biimpd 228 . . . . . . . . . . . 12 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∧ (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ∧ (𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐶 < (𝐶 + 𝑅) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))
7473exp32 422 . . . . . . . . . . 11 ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → ((𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐶 < (𝐶 + 𝑅) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))))
7574com4l 92 . . . . . . . . . 10 (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → ((𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐶 < (𝐶 + 𝑅) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))))
7633, 70, 71, 75syl3c 66 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))
77 fvex 6843 . . . . . . . . . . 11 ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) ∈ V
78 fvex 6843 . . . . . . . . . . 11 ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅)) ∈ V
7977, 78brcnv 5829 . . . . . . . . . 10 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅)) ↔ ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶))
8070fvresd 6850 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅)) = (𝐹‘(𝐶 + 𝑅)))
8180, 41breq12d 5110 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) ↔ (𝐹‘(𝐶 + 𝑅)) < (𝐹𝐶)))
8279, 81bitrid 283 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅)) ↔ (𝐹‘(𝐶 + 𝑅)) < (𝐹𝐶)))
8376, 82sylibd 238 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐹‘(𝐶 + 𝑅)) < (𝐹𝐶)))
84 funfvima2 7168 . . . . . . . . . . . . . 14 ((Fun 𝐹 ∧ ((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ dom 𝐹) → ((𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐹‘(𝐶 + 𝑅)) ∈ (𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))))
8545, 48, 84syl2anc 585 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐹‘(𝐶 + 𝑅)) ∈ (𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))))
8670, 85mpd 15 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹‘(𝐶 + 𝑅)) ∈ (𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅))))
8786, 54eleqtrd 2840 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹‘(𝐶 + 𝑅)) ∈ (𝑥[,]𝑦))
88 elicc2 13250 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝐹‘(𝐶 + 𝑅)) ∈ (𝑥[,]𝑦) ↔ ((𝐹‘(𝐶 + 𝑅)) ∈ ℝ ∧ 𝑥 ≤ (𝐹‘(𝐶 + 𝑅)) ∧ (𝐹‘(𝐶 + 𝑅)) ≤ 𝑦)))
8988ad2antrl 726 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹‘(𝐶 + 𝑅)) ∈ (𝑥[,]𝑦) ↔ ((𝐹‘(𝐶 + 𝑅)) ∈ ℝ ∧ 𝑥 ≤ (𝐹‘(𝐶 + 𝑅)) ∧ (𝐹‘(𝐶 + 𝑅)) ≤ 𝑦)))
9087, 89mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹‘(𝐶 + 𝑅)) ∈ ℝ ∧ 𝑥 ≤ (𝐹‘(𝐶 + 𝑅)) ∧ (𝐹‘(𝐶 + 𝑅)) ≤ 𝑦))
9190simp2d 1143 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝑥 ≤ (𝐹‘(𝐶 + 𝑅)))
9214, 69sseldd 3937 . . . . . . . . . . . 12 (𝜑 → (𝐶 + 𝑅) ∈ 𝑋)
9320, 92ffvelcdmd 7023 . . . . . . . . . . 11 (𝜑 → (𝐹‘(𝐶 + 𝑅)) ∈ ℝ)
9493adantr 482 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹‘(𝐶 + 𝑅)) ∈ ℝ)
95 lelttr 11171 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ (𝐹‘(𝐶 + 𝑅)) ∈ ℝ ∧ (𝐹𝐶) ∈ ℝ) → ((𝑥 ≤ (𝐹‘(𝐶 + 𝑅)) ∧ (𝐹‘(𝐶 + 𝑅)) < (𝐹𝐶)) → 𝑥 < (𝐹𝐶)))
9660, 94, 22, 95syl3anc 1371 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝑥 ≤ (𝐹‘(𝐶 + 𝑅)) ∧ (𝐹‘(𝐶 + 𝑅)) < (𝐹𝐶)) → 𝑥 < (𝐹𝐶)))
9791, 96mpand 693 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹‘(𝐶 + 𝑅)) < (𝐹𝐶) → 𝑥 < (𝐹𝐶)))
9883, 97syld 47 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → 𝑥 < (𝐹𝐶)))
99 ax-resscn 11034 . . . . . . . . . . . . . 14 ℝ ⊆ ℂ
10099a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ⊆ ℂ)
101 fss 6673 . . . . . . . . . . . . . 14 ((𝐹:𝑋⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:𝑋⟶ℂ)
10220, 99, 101sylancl 587 . . . . . . . . . . . . 13 (𝜑𝐹:𝑋⟶ℂ)
10314, 3sstrd 3946 . . . . . . . . . . . . 13 (𝜑 → ((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ ℝ)
104 eqid 2737 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
105104tgioo2 24072 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
106104, 105dvres 25181 . . . . . . . . . . . . 13 (((ℝ ⊆ ℂ ∧ 𝐹:𝑋⟶ℂ) ∧ (𝑋 ⊆ ℝ ∧ ((𝐶𝑅)[,](𝐶 + 𝑅)) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐶𝑅)[,](𝐶 + 𝑅)))))
107100, 102, 3, 103, 106syl22anc 837 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐶𝑅)[,](𝐶 + 𝑅)))))
108 iccntr 24090 . . . . . . . . . . . . . 14 (((𝐶𝑅) ∈ ℝ ∧ (𝐶 + 𝑅) ∈ ℝ) → ((int‘(topGen‘ran (,)))‘((𝐶𝑅)[,](𝐶 + 𝑅))) = ((𝐶𝑅)(,)(𝐶 + 𝑅)))
1098, 9, 108syl2anc 585 . . . . . . . . . . . . 13 (𝜑 → ((int‘(topGen‘ran (,)))‘((𝐶𝑅)[,](𝐶 + 𝑅))) = ((𝐶𝑅)(,)(𝐶 + 𝑅)))
110109reseq2d 5928 . . . . . . . . . . . 12 (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝐶𝑅)[,](𝐶 + 𝑅)))) = ((ℝ D 𝐹) ↾ ((𝐶𝑅)(,)(𝐶 + 𝑅))))
111107, 110eqtrd 2777 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) = ((ℝ D 𝐹) ↾ ((𝐶𝑅)(,)(𝐶 + 𝑅))))
112111dmeqd 5852 . . . . . . . . . 10 (𝜑 → dom (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) = dom ((ℝ D 𝐹) ↾ ((𝐶𝑅)(,)(𝐶 + 𝑅))))
113 dmres 5950 . . . . . . . . . . 11 dom ((ℝ D 𝐹) ↾ ((𝐶𝑅)(,)(𝐶 + 𝑅))) = (((𝐶𝑅)(,)(𝐶 + 𝑅)) ∩ dom (ℝ D 𝐹))
114 ioossicc 13271 . . . . . . . . . . . . . 14 ((𝐶𝑅)(,)(𝐶 + 𝑅)) ⊆ ((𝐶𝑅)[,](𝐶 + 𝑅))
115114, 14sstrid 3947 . . . . . . . . . . . . 13 (𝜑 → ((𝐶𝑅)(,)(𝐶 + 𝑅)) ⊆ 𝑋)
116115, 1sseqtrrd 3977 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝑅)(,)(𝐶 + 𝑅)) ⊆ dom (ℝ D 𝐹))
117 df-ss 3919 . . . . . . . . . . . 12 (((𝐶𝑅)(,)(𝐶 + 𝑅)) ⊆ dom (ℝ D 𝐹) ↔ (((𝐶𝑅)(,)(𝐶 + 𝑅)) ∩ dom (ℝ D 𝐹)) = ((𝐶𝑅)(,)(𝐶 + 𝑅)))
118116, 117sylib 217 . . . . . . . . . . 11 (𝜑 → (((𝐶𝑅)(,)(𝐶 + 𝑅)) ∩ dom (ℝ D 𝐹)) = ((𝐶𝑅)(,)(𝐶 + 𝑅)))
119113, 118eqtrid 2789 . . . . . . . . . 10 (𝜑 → dom ((ℝ D 𝐹) ↾ ((𝐶𝑅)(,)(𝐶 + 𝑅))) = ((𝐶𝑅)(,)(𝐶 + 𝑅)))
120112, 119eqtrd 2777 . . . . . . . . 9 (𝜑 → dom (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) = ((𝐶𝑅)(,)(𝐶 + 𝑅)))
121 resss 5953 . . . . . . . . . . . 12 ((ℝ D 𝐹) ↾ ((𝐶𝑅)(,)(𝐶 + 𝑅))) ⊆ (ℝ D 𝐹)
122111, 121eqsstrdi 3990 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ⊆ (ℝ D 𝐹))
123 rnss 5885 . . . . . . . . . . 11 ((ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ⊆ (ℝ D 𝐹) → ran (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ⊆ ran (ℝ D 𝐹))
124122, 123syl 17 . . . . . . . . . 10 (𝜑 → ran (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ⊆ ran (ℝ D 𝐹))
125 dvcnvre.z . . . . . . . . . 10 (𝜑 → ¬ 0 ∈ ran (ℝ D 𝐹))
126124, 125ssneldd 3939 . . . . . . . . 9 (𝜑 → ¬ 0 ∈ ran (ℝ D (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))))
1278, 9, 17, 120, 126dvne0 25281 . . . . . . . 8 (𝜑 → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∨ (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))))))
128127adantr 482 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∨ (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))))))
12967, 98, 128mpjaod 858 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝑥 < (𝐹𝐶))
130 isorel 7258 . . . . . . . . . . . . 13 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∧ (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ∧ (𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐶 < (𝐶 + 𝑅) ↔ ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))
131130biimpd 228 . . . . . . . . . . . 12 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∧ (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ∧ (𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐶 < (𝐶 + 𝑅) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))
132131exp32 422 . . . . . . . . . . 11 ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → ((𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐶 < (𝐶 + 𝑅) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))))
133132com4l 92 . . . . . . . . . 10 (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → ((𝐶 + 𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐶 < (𝐶 + 𝑅) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))))
13433, 70, 71, 133syl3c 66 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅))))
13541, 80breq12d 5110 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶 + 𝑅)) ↔ (𝐹𝐶) < (𝐹‘(𝐶 + 𝑅))))
136134, 135sylibd 238 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐹𝐶) < (𝐹‘(𝐶 + 𝑅))))
13790simp3d 1144 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹‘(𝐶 + 𝑅)) ≤ 𝑦)
138 simprlr 778 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝑦 ∈ ℝ)
139 ltletr 11173 . . . . . . . . . 10 (((𝐹𝐶) ∈ ℝ ∧ (𝐹‘(𝐶 + 𝑅)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝐹𝐶) < (𝐹‘(𝐶 + 𝑅)) ∧ (𝐹‘(𝐶 + 𝑅)) ≤ 𝑦) → (𝐹𝐶) < 𝑦))
14022, 94, 138, 139syl3anc 1371 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (((𝐹𝐶) < (𝐹‘(𝐶 + 𝑅)) ∧ (𝐹‘(𝐶 + 𝑅)) ≤ 𝑦) → (𝐹𝐶) < 𝑦))
141137, 140mpan2d 692 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹𝐶) < (𝐹‘(𝐶 + 𝑅)) → (𝐹𝐶) < 𝑦))
142136, 141syld 47 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐹𝐶) < 𝑦))
143 isorel 7258 . . . . . . . . . . . . 13 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∧ ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ∧ 𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐶𝑅) < 𝐶 ↔ ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))
144143biimpd 228 . . . . . . . . . . . 12 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) ∧ ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) ∧ 𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐶𝑅) < 𝐶 → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))
145144exp32 422 . . . . . . . . . . 11 ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → ((𝐶𝑅) < 𝐶 → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))))
146145com4l 92 . . . . . . . . . 10 ((𝐶𝑅) ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → (𝐶 ∈ ((𝐶𝑅)[,](𝐶 + 𝑅)) → ((𝐶𝑅) < 𝐶 → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))))
14727, 33, 34, 146syl3c 66 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶)))
148 fvex 6843 . . . . . . . . . . 11 ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) ∈ V
149148, 77brcnv 5829 . . . . . . . . . 10 (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) ↔ ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)))
15041, 40breq12d 5110 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) ↔ (𝐹𝐶) < (𝐹‘(𝐶𝑅))))
151149, 150bitrid 283 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘(𝐶𝑅)) < ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))‘𝐶) ↔ (𝐹𝐶) < (𝐹‘(𝐶𝑅))))
152147, 151sylibd 238 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐹𝐶) < (𝐹‘(𝐶𝑅))))
15358simp3d 1144 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹‘(𝐶𝑅)) ≤ 𝑦)
154 ltletr 11173 . . . . . . . . . 10 (((𝐹𝐶) ∈ ℝ ∧ (𝐹‘(𝐶𝑅)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝐹𝐶) < (𝐹‘(𝐶𝑅)) ∧ (𝐹‘(𝐶𝑅)) ≤ 𝑦) → (𝐹𝐶) < 𝑦))
15522, 63, 138, 154syl3anc 1371 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (((𝐹𝐶) < (𝐹‘(𝐶𝑅)) ∧ (𝐹‘(𝐶𝑅)) ≤ 𝑦) → (𝐹𝐶) < 𝑦))
156153, 155mpan2d 692 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹𝐶) < (𝐹‘(𝐶𝑅)) → (𝐹𝐶) < 𝑦))
157152, 156syld 47 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) Isom < , < (((𝐶𝑅)[,](𝐶 + 𝑅)), ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅)))) → (𝐹𝐶) < 𝑦))
158142, 157, 128mpjaod 858 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹𝐶) < 𝑦)
15960rexrd 11131 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝑥 ∈ ℝ*)
160138rexrd 11131 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → 𝑦 ∈ ℝ*)
161 elioo2 13226 . . . . . . 7 ((𝑥 ∈ ℝ*𝑦 ∈ ℝ*) → ((𝐹𝐶) ∈ (𝑥(,)𝑦) ↔ ((𝐹𝐶) ∈ ℝ ∧ 𝑥 < (𝐹𝐶) ∧ (𝐹𝐶) < 𝑦)))
162159, 160, 161syl2anc 585 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((𝐹𝐶) ∈ (𝑥(,)𝑦) ↔ ((𝐹𝐶) ∈ ℝ ∧ 𝑥 < (𝐹𝐶) ∧ (𝐹𝐶) < 𝑦)))
16322, 129, 158, 162mpbir3and 1342 . . . . 5 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹𝐶) ∈ (𝑥(,)𝑦))
16454fveq2d 6834 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))) = ((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦)))
165 iccntr 24090 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦)) = (𝑥(,)𝑦))
166165ad2antrl 726 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦)) = (𝑥(,)𝑦))
167164, 166eqtrd 2777 . . . . 5 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))) = (𝑥(,)𝑦))
168163, 167eleqtrrd 2841 . . . 4 ((𝜑 ∧ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦))) → (𝐹𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))))
169168expr 458 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦) → (𝐹𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅))))))
170169rexlimdvva 3202 . 2 (𝜑 → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ ran (𝐹 ↾ ((𝐶𝑅)[,](𝐶 + 𝑅))) = (𝑥[,]𝑦) → (𝐹𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅))))))
17118, 170mpd 15 1 (𝜑 → (𝐹𝐶) ∈ ((int‘(topGen‘ran (,)))‘(𝐹 “ ((𝐶𝑅)[,](𝐶 + 𝑅)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 845  w3a 1087   = wceq 1541  wcel 2106  wrex 3071  cin 3901  wss 3902   class class class wbr 5097  ccnv 5624  dom cdm 5625  ran crn 5626  cres 5627  cima 5628  Fun wfun 6478  wf 6480  1-1-ontowf1o 6483  cfv 6484   Isom wiso 6485  (class class class)co 7342  cc 10975  cr 10976  0cc0 10977   + caddc 10980  *cxr 11114   < clt 11115  cle 11116  cmin 11311  +crp 12836  (,)cioo 13185  [,]cicc 13188  TopOpenctopn 17230  topGenctg 17246  fldccnfld 20703  intcnt 22274  cnccncf 24145   D cdv 25133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-cnex 11033  ax-resscn 11034  ax-1cn 11035  ax-icn 11036  ax-addcl 11037  ax-addrcl 11038  ax-mulcl 11039  ax-mulrcl 11040  ax-mulcom 11041  ax-addass 11042  ax-mulass 11043  ax-distr 11044  ax-i2m1 11045  ax-1ne0 11046  ax-1rid 11047  ax-rnegex 11048  ax-rrecex 11049  ax-cnre 11050  ax-pre-lttri 11051  ax-pre-lttrn 11052  ax-pre-ltadd 11053  ax-pre-mulgt0 11054  ax-pre-sup 11055  ax-addf 11056  ax-mulf 11057
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4858  df-int 4900  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-se 5581  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-isom 6493  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-of 7600  df-om 7786  df-1st 7904  df-2nd 7905  df-supp 8053  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-1o 8372  df-2o 8373  df-er 8574  df-map 8693  df-pm 8694  df-ixp 8762  df-en 8810  df-dom 8811  df-sdom 8812  df-fin 8813  df-fsupp 9232  df-fi 9273  df-sup 9304  df-inf 9305  df-oi 9372  df-card 9801  df-pnf 11117  df-mnf 11118  df-xr 11119  df-ltxr 11120  df-le 11121  df-sub 11313  df-neg 11314  df-div 11739  df-nn 12080  df-2 12142  df-3 12143  df-4 12144  df-5 12145  df-6 12146  df-7 12147  df-8 12148  df-9 12149  df-n0 12340  df-z 12426  df-dec 12544  df-uz 12689  df-q 12795  df-rp 12837  df-xneg 12954  df-xadd 12955  df-xmul 12956  df-ioo 13189  df-ico 13191  df-icc 13192  df-fz 13346  df-fzo 13489  df-seq 13828  df-exp 13889  df-hash 14151  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-mulg 18798  df-cntz 19020  df-cmn 19484  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-cmp 22644  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-xms 23579  df-ms 23580  df-tms 23581  df-cncf 24147  df-limc 25136  df-dv 25137
This theorem is referenced by:  dvcnvrelem2  25288
  Copyright terms: Public domain W3C validator