Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cncfiooicclem1 Structured version   Visualization version   GIF version

Theorem cncfiooicclem1 45094
Description: A continuous function 𝐹 on an open interval (𝐴(,)𝐡) can be extended to a continuous function 𝐺 on the corresponding closed interval, if it has a finite right limit 𝑅 in 𝐴 and a finite left limit 𝐿 in 𝐡. 𝐹 can be complex-valued. This lemma assumes 𝐴 < 𝐡, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
cncfiooicclem1.x β„²π‘₯πœ‘
cncfiooicclem1.g 𝐺 = (π‘₯ ∈ (𝐴[,]𝐡) ↦ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))))
cncfiooicclem1.a (πœ‘ β†’ 𝐴 ∈ ℝ)
cncfiooicclem1.b (πœ‘ β†’ 𝐡 ∈ ℝ)
cncfiooicclem1.altb (πœ‘ β†’ 𝐴 < 𝐡)
cncfiooicclem1.f (πœ‘ β†’ 𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
cncfiooicclem1.l (πœ‘ β†’ 𝐿 ∈ (𝐹 limβ„‚ 𝐡))
cncfiooicclem1.r (πœ‘ β†’ 𝑅 ∈ (𝐹 limβ„‚ 𝐴))
Assertion
Ref Expression
cncfiooicclem1 (πœ‘ β†’ 𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐡   π‘₯,𝐹   π‘₯,𝐿   π‘₯,𝑅
Allowed substitution hints:   πœ‘(π‘₯)   𝐺(π‘₯)

Proof of Theorem cncfiooicclem1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 cncfiooicclem1.x . . . 4 β„²π‘₯πœ‘
2 limccl 25726 . . . . . . 7 (𝐹 limβ„‚ 𝐴) βŠ† β„‚
3 cncfiooicclem1.r . . . . . . 7 (πœ‘ β†’ 𝑅 ∈ (𝐹 limβ„‚ 𝐴))
42, 3sselid 3972 . . . . . 6 (πœ‘ β†’ 𝑅 ∈ β„‚)
54ad2antrr 723 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ π‘₯ = 𝐴) β†’ 𝑅 ∈ β„‚)
6 limccl 25726 . . . . . . . 8 (𝐹 limβ„‚ 𝐡) βŠ† β„‚
7 cncfiooicclem1.l . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ (𝐹 limβ„‚ 𝐡))
86, 7sselid 3972 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ β„‚)
98ad3antrrr 727 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ π‘₯ = 𝐡) β†’ 𝐿 ∈ β„‚)
10 simplll 772 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ πœ‘)
11 orel1 885 . . . . . . . . . . 11 (Β¬ π‘₯ = 𝐴 β†’ ((π‘₯ = 𝐴 ∨ π‘₯ = 𝐡) β†’ π‘₯ = 𝐡))
1211con3dimp 408 . . . . . . . . . 10 ((Β¬ π‘₯ = 𝐴 ∧ Β¬ π‘₯ = 𝐡) β†’ Β¬ (π‘₯ = 𝐴 ∨ π‘₯ = 𝐡))
13 vex 3470 . . . . . . . . . . 11 π‘₯ ∈ V
1413elpr 4643 . . . . . . . . . 10 (π‘₯ ∈ {𝐴, 𝐡} ↔ (π‘₯ = 𝐴 ∨ π‘₯ = 𝐡))
1512, 14sylnibr 329 . . . . . . . . 9 ((Β¬ π‘₯ = 𝐴 ∧ Β¬ π‘₯ = 𝐡) β†’ Β¬ π‘₯ ∈ {𝐴, 𝐡})
1615adantll 711 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ Β¬ π‘₯ ∈ {𝐴, 𝐡})
17 simpllr 773 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ π‘₯ ∈ (𝐴[,]𝐡))
18 cncfiooicclem1.a . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐴 ∈ ℝ)
1918rexrd 11261 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ ℝ*)
2010, 19syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ 𝐴 ∈ ℝ*)
21 cncfiooicclem1.b . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ ℝ)
2221rexrd 11261 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ ℝ*)
2310, 22syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ 𝐡 ∈ ℝ*)
24 cncfiooicclem1.altb . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐴 < 𝐡)
2518, 21, 24ltled 11359 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ≀ 𝐡)
2610, 25syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ 𝐴 ≀ 𝐡)
27 prunioo 13455 . . . . . . . . . . 11 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝐴 ≀ 𝐡) β†’ ((𝐴(,)𝐡) βˆͺ {𝐴, 𝐡}) = (𝐴[,]𝐡))
2820, 23, 26, 27syl3anc 1368 . . . . . . . . . 10 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ ((𝐴(,)𝐡) βˆͺ {𝐴, 𝐡}) = (𝐴[,]𝐡))
2917, 28eleqtrrd 2828 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ π‘₯ ∈ ((𝐴(,)𝐡) βˆͺ {𝐴, 𝐡}))
30 elun 4140 . . . . . . . . 9 (π‘₯ ∈ ((𝐴(,)𝐡) βˆͺ {𝐴, 𝐡}) ↔ (π‘₯ ∈ (𝐴(,)𝐡) ∨ π‘₯ ∈ {𝐴, 𝐡}))
3129, 30sylib 217 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ (π‘₯ ∈ (𝐴(,)𝐡) ∨ π‘₯ ∈ {𝐴, 𝐡}))
32 orel2 887 . . . . . . . 8 (Β¬ π‘₯ ∈ {𝐴, 𝐡} β†’ ((π‘₯ ∈ (𝐴(,)𝐡) ∨ π‘₯ ∈ {𝐴, 𝐡}) β†’ π‘₯ ∈ (𝐴(,)𝐡)))
3316, 31, 32sylc 65 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ π‘₯ ∈ (𝐴(,)𝐡))
34 cncfiooicclem1.f . . . . . . . . 9 (πœ‘ β†’ 𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
35 cncff 24735 . . . . . . . . 9 (𝐹 ∈ ((𝐴(,)𝐡)–cnβ†’β„‚) β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„‚)
3634, 35syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹:(𝐴(,)𝐡)βŸΆβ„‚)
3736ffvelcdmda 7076 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
3810, 33, 37syl2anc 583 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) ∧ Β¬ π‘₯ = 𝐡) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
399, 38ifclda 4555 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) ∧ Β¬ π‘₯ = 𝐴) β†’ if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)) ∈ β„‚)
405, 39ifclda 4555 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) ∈ β„‚)
41 cncfiooicclem1.g . . . 4 𝐺 = (π‘₯ ∈ (𝐴[,]𝐡) ↦ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))))
421, 40, 41fmptdf 7108 . . 3 (πœ‘ β†’ 𝐺:(𝐴[,]𝐡)βŸΆβ„‚)
43 elun 4140 . . . . . . 7 (𝑦 ∈ ((𝐴(,)𝐡) βˆͺ {𝐴, 𝐡}) ↔ (𝑦 ∈ (𝐴(,)𝐡) ∨ 𝑦 ∈ {𝐴, 𝐡}))
4419, 22, 25, 27syl3anc 1368 . . . . . . . 8 (πœ‘ β†’ ((𝐴(,)𝐡) βˆͺ {𝐴, 𝐡}) = (𝐴[,]𝐡))
4544eleq2d 2811 . . . . . . 7 (πœ‘ β†’ (𝑦 ∈ ((𝐴(,)𝐡) βˆͺ {𝐴, 𝐡}) ↔ 𝑦 ∈ (𝐴[,]𝐡)))
4643, 45bitr3id 285 . . . . . 6 (πœ‘ β†’ ((𝑦 ∈ (𝐴(,)𝐡) ∨ 𝑦 ∈ {𝐴, 𝐡}) ↔ 𝑦 ∈ (𝐴[,]𝐡)))
4746biimpar 477 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ (𝐴[,]𝐡)) β†’ (𝑦 ∈ (𝐴(,)𝐡) ∨ 𝑦 ∈ {𝐴, 𝐡}))
48 ioossicc 13407 . . . . . . . . . . . . 13 (𝐴(,)𝐡) βŠ† (𝐴[,]𝐡)
49 fssres 6747 . . . . . . . . . . . . 13 ((𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ (𝐴(,)𝐡) βŠ† (𝐴[,]𝐡)) β†’ (𝐺 β†Ύ (𝐴(,)𝐡)):(𝐴(,)𝐡)βŸΆβ„‚)
5042, 48, 49sylancl 585 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)):(𝐴(,)𝐡)βŸΆβ„‚)
5150feqmptd 6950 . . . . . . . . . . 11 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) = (𝑦 ∈ (𝐴(,)𝐡) ↦ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘¦)))
52 nfmpt1 5246 . . . . . . . . . . . . . . . 16 β„²π‘₯(π‘₯ ∈ (𝐴[,]𝐡) ↦ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))))
5341, 52nfcxfr 2893 . . . . . . . . . . . . . . 15 β„²π‘₯𝐺
54 nfcv 2895 . . . . . . . . . . . . . . 15 β„²π‘₯(𝐴(,)𝐡)
5553, 54nfres 5973 . . . . . . . . . . . . . 14 β„²π‘₯(𝐺 β†Ύ (𝐴(,)𝐡))
56 nfcv 2895 . . . . . . . . . . . . . 14 β„²π‘₯𝑦
5755, 56nffv 6891 . . . . . . . . . . . . 13 β„²π‘₯((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘¦)
58 nfcv 2895 . . . . . . . . . . . . . 14 Ⅎ𝑦(𝐺 β†Ύ (𝐴(,)𝐡))
59 nfcv 2895 . . . . . . . . . . . . . 14 Ⅎ𝑦π‘₯
6058, 59nffv 6891 . . . . . . . . . . . . 13 Ⅎ𝑦((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘₯)
61 fveq2 6881 . . . . . . . . . . . . 13 (𝑦 = π‘₯ β†’ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘¦) = ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘₯))
6257, 60, 61cbvmpt 5249 . . . . . . . . . . . 12 (𝑦 ∈ (𝐴(,)𝐡) ↦ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘¦)) = (π‘₯ ∈ (𝐴(,)𝐡) ↦ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘₯))
6362a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝑦 ∈ (𝐴(,)𝐡) ↦ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘¦)) = (π‘₯ ∈ (𝐴(,)𝐡) ↦ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘₯)))
64 fvres 6900 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴(,)𝐡) β†’ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘₯) = (πΊβ€˜π‘₯))
6564adantl 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘₯) = (πΊβ€˜π‘₯))
66 simpr 484 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ π‘₯ ∈ (𝐴(,)𝐡))
6748, 66sselid 3972 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ π‘₯ ∈ (𝐴[,]𝐡))
684adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ 𝑅 ∈ β„‚)
698ad2antrr 723 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) ∧ π‘₯ = 𝐡) β†’ 𝐿 ∈ β„‚)
7037adantr 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) ∧ Β¬ π‘₯ = 𝐡) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
7169, 70ifclda 4555 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)) ∈ β„‚)
7268, 71ifcld 4566 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) ∈ β„‚)
7341fvmpt2 6999 . . . . . . . . . . . . . 14 ((π‘₯ ∈ (𝐴[,]𝐡) ∧ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) ∈ β„‚) β†’ (πΊβ€˜π‘₯) = if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))))
7467, 72, 73syl2anc 583 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (πΊβ€˜π‘₯) = if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))))
75 elioo4g 13381 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (𝐴(,)𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ π‘₯ ∈ ℝ) ∧ (𝐴 < π‘₯ ∧ π‘₯ < 𝐡)))
7675biimpi 215 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (𝐴(,)𝐡) β†’ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ π‘₯ ∈ ℝ) ∧ (𝐴 < π‘₯ ∧ π‘₯ < 𝐡)))
7776simpld 494 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (𝐴(,)𝐡) β†’ (𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ π‘₯ ∈ ℝ))
7877simp1d 1139 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴(,)𝐡) β†’ 𝐴 ∈ ℝ*)
79 elioore 13351 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (𝐴(,)𝐡) β†’ π‘₯ ∈ ℝ)
8079rexrd 11261 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴(,)𝐡) β†’ π‘₯ ∈ ℝ*)
81 eliooord 13380 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (𝐴(,)𝐡) β†’ (𝐴 < π‘₯ ∧ π‘₯ < 𝐡))
8281simpld 494 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴(,)𝐡) β†’ 𝐴 < π‘₯)
83 xrltne 13139 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ* ∧ π‘₯ ∈ ℝ* ∧ 𝐴 < π‘₯) β†’ π‘₯ β‰  𝐴)
8478, 80, 82, 83syl3anc 1368 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴(,)𝐡) β†’ π‘₯ β‰  𝐴)
8584adantl 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ π‘₯ β‰  𝐴)
8685neneqd 2937 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ Β¬ π‘₯ = 𝐴)
8786iffalsed 4531 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)))
8881simprd 495 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴(,)𝐡) β†’ π‘₯ < 𝐡)
8979, 88ltned 11347 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴(,)𝐡) β†’ π‘₯ β‰  𝐡)
9089neneqd 2937 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝐴(,)𝐡) β†’ Β¬ π‘₯ = 𝐡)
9190iffalsed 4531 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴(,)𝐡) β†’ if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)) = (πΉβ€˜π‘₯))
9291adantl 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)) = (πΉβ€˜π‘₯))
9387, 92eqtrd 2764 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = (πΉβ€˜π‘₯))
9465, 74, 933eqtrd 2768 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘₯) = (πΉβ€˜π‘₯))
951, 94mpteq2da 5236 . . . . . . . . . . 11 (πœ‘ β†’ (π‘₯ ∈ (𝐴(,)𝐡) ↦ ((𝐺 β†Ύ (𝐴(,)𝐡))β€˜π‘₯)) = (π‘₯ ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜π‘₯)))
9651, 63, 953eqtrd 2768 . . . . . . . . . 10 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) = (π‘₯ ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜π‘₯)))
9736feqmptd 6950 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜π‘₯)))
98 ioosscn 13383 . . . . . . . . . . . . 13 (𝐴(,)𝐡) βŠ† β„‚
9998a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† β„‚)
100 ssid 3996 . . . . . . . . . . . 12 β„‚ βŠ† β„‚
101 eqid 2724 . . . . . . . . . . . . 13 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
102 eqid 2724 . . . . . . . . . . . . 13 ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) = ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡))
103101cnfldtop 24622 . . . . . . . . . . . . . . 15 (TopOpenβ€˜β„‚fld) ∈ Top
104 unicntop 24624 . . . . . . . . . . . . . . . 16 β„‚ = βˆͺ (TopOpenβ€˜β„‚fld)
105104restid 17378 . . . . . . . . . . . . . . 15 ((TopOpenβ€˜β„‚fld) ∈ Top β†’ ((TopOpenβ€˜β„‚fld) β†Ύt β„‚) = (TopOpenβ€˜β„‚fld))
106103, 105ax-mp 5 . . . . . . . . . . . . . 14 ((TopOpenβ€˜β„‚fld) β†Ύt β„‚) = (TopOpenβ€˜β„‚fld)
107106eqcomi 2733 . . . . . . . . . . . . 13 (TopOpenβ€˜β„‚fld) = ((TopOpenβ€˜β„‚fld) β†Ύt β„‚)
108101, 102, 107cncfcn 24752 . . . . . . . . . . . 12 (((𝐴(,)𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((𝐴(,)𝐡)–cnβ†’β„‚) = (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) Cn (TopOpenβ€˜β„‚fld)))
10999, 100, 108sylancl 585 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐴(,)𝐡)–cnβ†’β„‚) = (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) Cn (TopOpenβ€˜β„‚fld)))
11034, 97, 1093eltr3d 2839 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜π‘₯)) ∈ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) Cn (TopOpenβ€˜β„‚fld)))
11196, 110eqeltrd 2825 . . . . . . . . 9 (πœ‘ β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) Cn (TopOpenβ€˜β„‚fld)))
112104restuni 22988 . . . . . . . . . . 11 (((TopOpenβ€˜β„‚fld) ∈ Top ∧ (𝐴(,)𝐡) βŠ† β„‚) β†’ (𝐴(,)𝐡) = βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)))
113103, 98, 112mp2an 689 . . . . . . . . . 10 (𝐴(,)𝐡) = βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡))
114113cncnpi 23104 . . . . . . . . 9 (((𝐺 β†Ύ (𝐴(,)𝐡)) ∈ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) Cn (TopOpenβ€˜β„‚fld)) ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
115111, 114sylan 579 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
116103a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (TopOpenβ€˜β„‚fld) ∈ Top)
11748a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐴(,)𝐡) βŠ† (𝐴[,]𝐡))
118 ovex 7434 . . . . . . . . . . . . 13 (𝐴[,]𝐡) ∈ V
119118a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐴[,]𝐡) ∈ V)
120 restabs 22991 . . . . . . . . . . . 12 (((TopOpenβ€˜β„‚fld) ∈ Top ∧ (𝐴(,)𝐡) βŠ† (𝐴[,]𝐡) ∧ (𝐴[,]𝐡) ∈ V) β†’ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) β†Ύt (𝐴(,)𝐡)) = ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)))
121116, 117, 119, 120syl3anc 1368 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) β†Ύt (𝐴(,)𝐡)) = ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)))
122121eqcomd 2730 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) = (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) β†Ύt (𝐴(,)𝐡)))
123122oveq1d 7416 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld)) = ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld)))
124123fveq1d 6883 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦) = (((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
125115, 124eleqtrd 2827 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ (((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
126 resttop 22986 . . . . . . . . . 10 (((TopOpenβ€˜β„‚fld) ∈ Top ∧ (𝐴[,]𝐡) ∈ V) β†’ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) ∈ Top)
127103, 118, 126mp2an 689 . . . . . . . . 9 ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) ∈ Top
128127a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) ∈ Top)
12948a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† (𝐴[,]𝐡))
13018, 21iccssred 13408 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
131 ax-resscn 11163 . . . . . . . . . . . 12 ℝ βŠ† β„‚
132130, 131sstrdi 3986 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† β„‚)
133104restuni 22988 . . . . . . . . . . 11 (((TopOpenβ€˜β„‚fld) ∈ Top ∧ (𝐴[,]𝐡) βŠ† β„‚) β†’ (𝐴[,]𝐡) = βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))
134103, 132, 133sylancr 586 . . . . . . . . . 10 (πœ‘ β†’ (𝐴[,]𝐡) = βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))
135129, 134sseqtrd 4014 . . . . . . . . 9 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))
136135adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐴(,)𝐡) βŠ† βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))
137 retop 24600 . . . . . . . . . . . . . 14 (topGenβ€˜ran (,)) ∈ Top
138137a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (topGenβ€˜ran (,)) ∈ Top)
139 ioossre 13382 . . . . . . . . . . . . . . 15 (𝐴(,)𝐡) βŠ† ℝ
140 difss 4123 . . . . . . . . . . . . . . 15 (ℝ βˆ– (𝐴[,]𝐡)) βŠ† ℝ
141139, 140unssi 4177 . . . . . . . . . . . . . 14 ((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡))) βŠ† ℝ
142141a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ ((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡))) βŠ† ℝ)
143 ssun1 4164 . . . . . . . . . . . . . 14 (𝐴(,)𝐡) βŠ† ((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡)))
144143a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐴(,)𝐡) βŠ† ((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡))))
145 uniretop 24601 . . . . . . . . . . . . . 14 ℝ = βˆͺ (topGenβ€˜ran (,))
146145ntrss 22881 . . . . . . . . . . . . 13 (((topGenβ€˜ran (,)) ∈ Top ∧ ((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡))) βŠ† ℝ ∧ (𝐴(,)𝐡) βŠ† ((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡)))) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴(,)𝐡)) βŠ† ((intβ€˜(topGenβ€˜ran (,)))β€˜((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡)))))
147138, 142, 144, 146syl3anc 1368 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴(,)𝐡)) βŠ† ((intβ€˜(topGenβ€˜ran (,)))β€˜((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡)))))
148 simpr 484 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝑦 ∈ (𝐴(,)𝐡))
149 ioontr 44709 . . . . . . . . . . . . 13 ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴(,)𝐡)) = (𝐴(,)𝐡)
150148, 149eleqtrrdi 2836 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝑦 ∈ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴(,)𝐡)))
151147, 150sseldd 3975 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝑦 ∈ ((intβ€˜(topGenβ€˜ran (,)))β€˜((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡)))))
15248, 148sselid 3972 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝑦 ∈ (𝐴[,]𝐡))
153151, 152elind 4186 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝑦 ∈ (((intβ€˜(topGenβ€˜ran (,)))β€˜((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡)))) ∩ (𝐴[,]𝐡)))
154130adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐴[,]𝐡) βŠ† ℝ)
155 eqid 2724 . . . . . . . . . . . 12 ((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡)) = ((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡))
156145, 155restntr 23008 . . . . . . . . . . 11 (((topGenβ€˜ran (,)) ∈ Top ∧ (𝐴[,]𝐡) βŠ† ℝ ∧ (𝐴(,)𝐡) βŠ† (𝐴[,]𝐡)) β†’ ((intβ€˜((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)) = (((intβ€˜(topGenβ€˜ran (,)))β€˜((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡)))) ∩ (𝐴[,]𝐡)))
157138, 154, 117, 156syl3anc 1368 . . . . . . . . . 10 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ ((intβ€˜((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)) = (((intβ€˜(topGenβ€˜ran (,)))β€˜((𝐴(,)𝐡) βˆͺ (ℝ βˆ– (𝐴[,]𝐡)))) ∩ (𝐴[,]𝐡)))
158153, 157eleqtrrd 2828 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝑦 ∈ ((intβ€˜((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)))
159101tgioo2 24641 . . . . . . . . . . . . . . 15 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
160159a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ))
161160oveq1d 7416 . . . . . . . . . . . . 13 (πœ‘ β†’ ((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡)) = (((TopOpenβ€˜β„‚fld) β†Ύt ℝ) β†Ύt (𝐴[,]𝐡)))
162103a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ (TopOpenβ€˜β„‚fld) ∈ Top)
163 reex 11197 . . . . . . . . . . . . . . 15 ℝ ∈ V
164163a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ ℝ ∈ V)
165 restabs 22991 . . . . . . . . . . . . . 14 (((TopOpenβ€˜β„‚fld) ∈ Top ∧ (𝐴[,]𝐡) βŠ† ℝ ∧ ℝ ∈ V) β†’ (((TopOpenβ€˜β„‚fld) β†Ύt ℝ) β†Ύt (𝐴[,]𝐡)) = ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))
166162, 130, 164, 165syl3anc 1368 . . . . . . . . . . . . 13 (πœ‘ β†’ (((TopOpenβ€˜β„‚fld) β†Ύt ℝ) β†Ύt (𝐴[,]𝐡)) = ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))
167161, 166eqtrd 2764 . . . . . . . . . . . 12 (πœ‘ β†’ ((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡)) = ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))
168167fveq2d 6885 . . . . . . . . . . 11 (πœ‘ β†’ (intβ€˜((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡))) = (intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡))))
169168fveq1d 6883 . . . . . . . . . 10 (πœ‘ β†’ ((intβ€˜((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)) = ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)))
170169adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ ((intβ€˜((topGenβ€˜ran (,)) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)) = ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)))
171158, 170eleqtrd 2827 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝑦 ∈ ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)))
172134feq2d 6693 . . . . . . . . . 10 (πœ‘ β†’ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ↔ 𝐺:βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡))βŸΆβ„‚))
17342, 172mpbid 231 . . . . . . . . 9 (πœ‘ β†’ 𝐺:βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡))βŸΆβ„‚)
174173adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝐺:βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡))βŸΆβ„‚)
175 eqid 2724 . . . . . . . . 9 βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) = βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡))
176175, 104cnprest 23115 . . . . . . . 8 (((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) ∈ Top ∧ (𝐴(,)𝐡) βŠ† βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡))) ∧ (𝑦 ∈ ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)))β€˜(𝐴(,)𝐡)) ∧ 𝐺:βˆͺ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡))βŸΆβ„‚)) β†’ (𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦) ↔ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ (((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦)))
177128, 136, 171, 174, 176syl22anc 836 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ (𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦) ↔ (𝐺 β†Ύ (𝐴(,)𝐡)) ∈ (((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) β†Ύt (𝐴(,)𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦)))
178125, 177mpbird 257 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ (𝐴(,)𝐡)) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
179 elpri 4642 . . . . . . 7 (𝑦 ∈ {𝐴, 𝐡} β†’ (𝑦 = 𝐴 ∨ 𝑦 = 𝐡))
180 iftrue 4526 . . . . . . . . . . . . 13 (π‘₯ = 𝐴 β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = 𝑅)
181 lbicc2 13438 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝐴 ≀ 𝐡) β†’ 𝐴 ∈ (𝐴[,]𝐡))
18219, 22, 25, 181syl3anc 1368 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐴 ∈ (𝐴[,]𝐡))
18341, 180, 182, 3fvmptd3 7011 . . . . . . . . . . . 12 (πœ‘ β†’ (πΊβ€˜π΄) = 𝑅)
18497eqcomd 2730 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘₯ ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜π‘₯)) = 𝐹)
18596, 184eqtr2d 2765 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 = (𝐺 β†Ύ (𝐴(,)𝐡)))
186185oveq1d 7416 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐹 limβ„‚ 𝐴) = ((𝐺 β†Ύ (𝐴(,)𝐡)) limβ„‚ 𝐴))
1873, 186eleqtrd 2827 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑅 ∈ ((𝐺 β†Ύ (𝐴(,)𝐡)) limβ„‚ 𝐴))
18818, 21, 24, 42limciccioolb 44822 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐺 β†Ύ (𝐴(,)𝐡)) limβ„‚ 𝐴) = (𝐺 limβ„‚ 𝐴))
189187, 188eleqtrd 2827 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑅 ∈ (𝐺 limβ„‚ 𝐴))
190183, 189eqeltrd 2825 . . . . . . . . . . 11 (πœ‘ β†’ (πΊβ€˜π΄) ∈ (𝐺 limβ„‚ 𝐴))
191 eqid 2724 . . . . . . . . . . . . 13 ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) = ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡))
192101, 191cnplimc 25738 . . . . . . . . . . . 12 (((𝐴[,]𝐡) βŠ† β„‚ ∧ 𝐴 ∈ (𝐴[,]𝐡)) β†’ (𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΄) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ (πΊβ€˜π΄) ∈ (𝐺 limβ„‚ 𝐴))))
193132, 182, 192syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ (𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΄) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ (πΊβ€˜π΄) ∈ (𝐺 limβ„‚ 𝐴))))
19442, 190, 193mpbir2and 710 . . . . . . . . . 10 (πœ‘ β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΄))
195194adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 = 𝐴) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΄))
196 fveq2 6881 . . . . . . . . . . 11 (𝑦 = 𝐴 β†’ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦) = ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΄))
197196eqcomd 2730 . . . . . . . . . 10 (𝑦 = 𝐴 β†’ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΄) = ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
198197adantl 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 = 𝐴) β†’ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΄) = ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
199195, 198eleqtrd 2827 . . . . . . . 8 ((πœ‘ ∧ 𝑦 = 𝐴) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
200180adantl 481 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝐡 ∧ π‘₯ = 𝐴) β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = 𝑅)
201 eqtr2 2748 . . . . . . . . . . . . . . . . 17 ((π‘₯ = 𝐡 ∧ π‘₯ = 𝐴) β†’ 𝐡 = 𝐴)
202 iftrue 4526 . . . . . . . . . . . . . . . . . 18 (𝐡 = 𝐴 β†’ if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))) = 𝑅)
203202eqcomd 2730 . . . . . . . . . . . . . . . . 17 (𝐡 = 𝐴 β†’ 𝑅 = if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))))
204201, 203syl 17 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝐡 ∧ π‘₯ = 𝐴) β†’ 𝑅 = if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))))
205200, 204eqtrd 2764 . . . . . . . . . . . . . . 15 ((π‘₯ = 𝐡 ∧ π‘₯ = 𝐴) β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))))
206 iffalse 4529 . . . . . . . . . . . . . . . . 17 (Β¬ π‘₯ = 𝐴 β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)))
207206adantl 481 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝐡 ∧ Β¬ π‘₯ = 𝐴) β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)))
208 iftrue 4526 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝐡 β†’ if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)) = 𝐿)
209208adantr 480 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝐡 ∧ Β¬ π‘₯ = 𝐴) β†’ if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯)) = 𝐿)
210 df-ne 2933 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ β‰  𝐴 ↔ Β¬ π‘₯ = 𝐴)
211 pm13.18 3014 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ = 𝐡 ∧ π‘₯ β‰  𝐴) β†’ 𝐡 β‰  𝐴)
212210, 211sylan2br 594 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ = 𝐡 ∧ Β¬ π‘₯ = 𝐴) β†’ 𝐡 β‰  𝐴)
213212neneqd 2937 . . . . . . . . . . . . . . . . . 18 ((π‘₯ = 𝐡 ∧ Β¬ π‘₯ = 𝐴) β†’ Β¬ 𝐡 = 𝐴)
214213iffalsed 4531 . . . . . . . . . . . . . . . . 17 ((π‘₯ = 𝐡 ∧ Β¬ π‘₯ = 𝐴) β†’ if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))) = if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅)))
215 eqid 2724 . . . . . . . . . . . . . . . . . 18 𝐡 = 𝐡
216215iftruei 4527 . . . . . . . . . . . . . . . . 17 if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅)) = 𝐿
217214, 216eqtr2di 2781 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝐡 ∧ Β¬ π‘₯ = 𝐴) β†’ 𝐿 = if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))))
218207, 209, 2173eqtrd 2768 . . . . . . . . . . . . . . 15 ((π‘₯ = 𝐡 ∧ Β¬ π‘₯ = 𝐴) β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))))
219205, 218pm2.61dan 810 . . . . . . . . . . . . . 14 (π‘₯ = 𝐡 β†’ if(π‘₯ = 𝐴, 𝑅, if(π‘₯ = 𝐡, 𝐿, (πΉβ€˜π‘₯))) = if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))))
22021leidd 11777 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐡 ≀ 𝐡)
22118, 21, 21, 25, 220eliccd 44702 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐡 ∈ (𝐴[,]𝐡))
222216, 8eqeltrid 2829 . . . . . . . . . . . . . . 15 (πœ‘ β†’ if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅)) ∈ β„‚)
2234, 222ifcld 4566 . . . . . . . . . . . . . 14 (πœ‘ β†’ if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))) ∈ β„‚)
22441, 219, 221, 223fvmptd3 7011 . . . . . . . . . . . . 13 (πœ‘ β†’ (πΊβ€˜π΅) = if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))))
22518, 24gtned 11346 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐡 β‰  𝐴)
226225neneqd 2937 . . . . . . . . . . . . . 14 (πœ‘ β†’ Β¬ 𝐡 = 𝐴)
227226iffalsed 4531 . . . . . . . . . . . . 13 (πœ‘ β†’ if(𝐡 = 𝐴, 𝑅, if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅))) = if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅)))
228216a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ if(𝐡 = 𝐡, 𝐿, (πΉβ€˜π΅)) = 𝐿)
229224, 227, 2283eqtrd 2768 . . . . . . . . . . . 12 (πœ‘ β†’ (πΊβ€˜π΅) = 𝐿)
230185oveq1d 7416 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐹 limβ„‚ 𝐡) = ((𝐺 β†Ύ (𝐴(,)𝐡)) limβ„‚ 𝐡))
2317, 230eleqtrd 2827 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 ∈ ((𝐺 β†Ύ (𝐴(,)𝐡)) limβ„‚ 𝐡))
23218, 21, 24, 42limcicciooub 44838 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐺 β†Ύ (𝐴(,)𝐡)) limβ„‚ 𝐡) = (𝐺 limβ„‚ 𝐡))
233231, 232eleqtrd 2827 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐿 ∈ (𝐺 limβ„‚ 𝐡))
234229, 233eqeltrd 2825 . . . . . . . . . . 11 (πœ‘ β†’ (πΊβ€˜π΅) ∈ (𝐺 limβ„‚ 𝐡))
235101, 191cnplimc 25738 . . . . . . . . . . . 12 (((𝐴[,]𝐡) βŠ† β„‚ ∧ 𝐡 ∈ (𝐴[,]𝐡)) β†’ (𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΅) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ (πΊβ€˜π΅) ∈ (𝐺 limβ„‚ 𝐡))))
236132, 221, 235syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ (𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΅) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ (πΊβ€˜π΅) ∈ (𝐺 limβ„‚ 𝐡))))
23742, 234, 236mpbir2and 710 . . . . . . . . . 10 (πœ‘ β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΅))
238237adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 = 𝐡) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΅))
239 fveq2 6881 . . . . . . . . . . 11 (𝑦 = 𝐡 β†’ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦) = ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΅))
240239eqcomd 2730 . . . . . . . . . 10 (𝑦 = 𝐡 β†’ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΅) = ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
241240adantl 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑦 = 𝐡) β†’ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π΅) = ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
242238, 241eleqtrd 2827 . . . . . . . 8 ((πœ‘ ∧ 𝑦 = 𝐡) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
243199, 242jaodan 954 . . . . . . 7 ((πœ‘ ∧ (𝑦 = 𝐴 ∨ 𝑦 = 𝐡)) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
244179, 243sylan2 592 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ {𝐴, 𝐡}) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
245178, 244jaodan 954 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ (𝐴(,)𝐡) ∨ 𝑦 ∈ {𝐴, 𝐡})) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
24647, 245syldan 590 . . . 4 ((πœ‘ ∧ 𝑦 ∈ (𝐴[,]𝐡)) β†’ 𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
247246ralrimiva 3138 . . 3 (πœ‘ β†’ βˆ€π‘¦ ∈ (𝐴[,]𝐡)𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))
248101cnfldtopon 24621 . . . . 5 (TopOpenβ€˜β„‚fld) ∈ (TopOnβ€˜β„‚)
249 resttopon 22987 . . . . 5 (((TopOpenβ€˜β„‚fld) ∈ (TopOnβ€˜β„‚) ∧ (𝐴[,]𝐡) βŠ† β„‚) β†’ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) ∈ (TopOnβ€˜(𝐴[,]𝐡)))
250248, 132, 249sylancr 586 . . . 4 (πœ‘ β†’ ((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) ∈ (TopOnβ€˜(𝐴[,]𝐡)))
251 cncnp 23106 . . . 4 ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) ∈ (TopOnβ€˜(𝐴[,]𝐡)) ∧ (TopOpenβ€˜β„‚fld) ∈ (TopOnβ€˜β„‚)) β†’ (𝐺 ∈ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) Cn (TopOpenβ€˜β„‚fld)) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ βˆ€π‘¦ ∈ (𝐴[,]𝐡)𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))))
252250, 248, 251sylancl 585 . . 3 (πœ‘ β†’ (𝐺 ∈ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) Cn (TopOpenβ€˜β„‚fld)) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ βˆ€π‘¦ ∈ (𝐴[,]𝐡)𝐺 ∈ ((((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) CnP (TopOpenβ€˜β„‚fld))β€˜π‘¦))))
25342, 247, 252mpbir2and 710 . 2 (πœ‘ β†’ 𝐺 ∈ (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) Cn (TopOpenβ€˜β„‚fld)))
254101, 191, 107cncfcn 24752 . . 3 (((𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ ((𝐴[,]𝐡)–cnβ†’β„‚) = (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) Cn (TopOpenβ€˜β„‚fld)))
255132, 100, 254sylancl 585 . 2 (πœ‘ β†’ ((𝐴[,]𝐡)–cnβ†’β„‚) = (((TopOpenβ€˜β„‚fld) β†Ύt (𝐴[,]𝐡)) Cn (TopOpenβ€˜β„‚fld)))
256253, 255eleqtrrd 2828 1 (πœ‘ β†’ 𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1084   = wceq 1533  β„²wnf 1777   ∈ wcel 2098   β‰  wne 2932  βˆ€wral 3053  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  ifcif 4520  {cpr 4622  βˆͺ cuni 4899   class class class wbr 5138   ↦ cmpt 5221  ran crn 5667   β†Ύ cres 5668  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401  β„‚cc 11104  β„cr 11105  β„*cxr 11244   < clt 11245   ≀ cle 11246  (,)cioo 13321  [,]cicc 13324   β†Ύt crest 17365  TopOpenctopn 17366  topGenctg 17382  β„‚fldccnfld 21228  Topctop 22717  TopOnctopon 22734  intcnt 22843   Cn ccn 23050   CnP ccnp 23051  β€“cnβ†’ccncf 24718   limβ„‚ climc 25713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fi 9402  df-sup 9433  df-inf 9434  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-struct 17079  df-slot 17114  df-ndx 17126  df-base 17144  df-plusg 17209  df-mulr 17210  df-starv 17211  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-rest 17367  df-topn 17368  df-topgen 17388  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-cn 23053  df-cnp 23054  df-xms 24148  df-ms 24149  df-cncf 24720  df-limc 25717
This theorem is referenced by:  cncfiooicc  45095
  Copyright terms: Public domain W3C validator