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

Theorem limciun 25274
Description: A point is a limit of 𝐹 on the finite union βˆͺ π‘₯ ∈ 𝐴𝐡(π‘₯) iff it is the limit of the restriction of 𝐹 to each 𝐡(π‘₯). (Contributed by Mario Carneiro, 30-Dec-2016.)
Hypotheses
Ref Expression
limciun.1 (πœ‘ β†’ 𝐴 ∈ Fin)
limciun.2 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† β„‚)
limciun.3 (πœ‘ β†’ 𝐹:βˆͺ π‘₯ ∈ 𝐴 π΅βŸΆβ„‚)
limciun.4 (πœ‘ β†’ 𝐢 ∈ β„‚)
Assertion
Ref Expression
limciun (πœ‘ β†’ (𝐹 limβ„‚ 𝐢) = (β„‚ ∩ ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐢   π‘₯,𝐹
Allowed substitution hints:   πœ‘(π‘₯)   𝐡(π‘₯)

Proof of Theorem limciun
Dummy variables 𝑔 π‘Ž π‘˜ 𝑒 𝑣 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 25255 . . . 4 (𝐹 limβ„‚ 𝐢) βŠ† β„‚
2 limcresi 25265 . . . . . 6 (𝐹 limβ„‚ 𝐢) βŠ† ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)
32rgenw 3069 . . . . 5 βˆ€π‘₯ ∈ 𝐴 (𝐹 limβ„‚ 𝐢) βŠ† ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)
4 ssiin 5020 . . . . 5 ((𝐹 limβ„‚ 𝐢) βŠ† ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢) ↔ βˆ€π‘₯ ∈ 𝐴 (𝐹 limβ„‚ 𝐢) βŠ† ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))
53, 4mpbir 230 . . . 4 (𝐹 limβ„‚ 𝐢) βŠ† ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)
61, 5ssini 4196 . . 3 (𝐹 limβ„‚ 𝐢) βŠ† (β„‚ ∩ ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))
76a1i 11 . 2 (πœ‘ β†’ (𝐹 limβ„‚ 𝐢) βŠ† (β„‚ ∩ ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)))
8 elriin 5046 . . . 4 (𝑦 ∈ (β„‚ ∩ ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)) ↔ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)))
9 simprl 770 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) β†’ 𝑦 ∈ β„‚)
10 limciun.1 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ Fin)
1110ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) β†’ 𝐴 ∈ Fin)
12 simplrr 777 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) β†’ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))
13 nfcv 2908 . . . . . . . . . . . . . . . . . . . 20 β„²π‘₯𝐹
14 nfcsb1v 3885 . . . . . . . . . . . . . . . . . . . 20 β„²π‘₯β¦‹π‘Ž / π‘₯⦌𝐡
1513, 14nfres 5944 . . . . . . . . . . . . . . . . . . 19 β„²π‘₯(𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡)
16 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 β„²π‘₯ limβ„‚
17 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 β„²π‘₯𝐢
1815, 16, 17nfov 7392 . . . . . . . . . . . . . . . . . 18 β„²π‘₯((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) limβ„‚ 𝐢)
1918nfcri 2895 . . . . . . . . . . . . . . . . 17 β„²π‘₯ 𝑦 ∈ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) limβ„‚ 𝐢)
20 csbeq1a 3874 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = π‘Ž β†’ 𝐡 = β¦‹π‘Ž / π‘₯⦌𝐡)
2120reseq2d 5942 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = π‘Ž β†’ (𝐹 β†Ύ 𝐡) = (𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡))
2221oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Ž β†’ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢) = ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) limβ„‚ 𝐢))
2322eleq2d 2824 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Ž β†’ (𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢) ↔ 𝑦 ∈ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) limβ„‚ 𝐢)))
2419, 23rspc 3572 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ 𝐴 β†’ (βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢) β†’ 𝑦 ∈ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) limβ„‚ 𝐢)))
2512, 24mpan9 508 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ π‘Ž ∈ 𝐴) β†’ 𝑦 ∈ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) limβ„‚ 𝐢))
26 limciun.3 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐹:βˆͺ π‘₯ ∈ 𝐴 π΅βŸΆβ„‚)
2726ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ π‘Ž ∈ 𝐴) β†’ 𝐹:βˆͺ π‘₯ ∈ 𝐴 π΅βŸΆβ„‚)
28 ssiun2 5012 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž ∈ 𝐴 β†’ β¦‹π‘Ž / π‘₯⦌𝐡 βŠ† βˆͺ π‘Ž ∈ 𝐴 β¦‹π‘Ž / π‘₯⦌𝐡)
29 nfcv 2908 . . . . . . . . . . . . . . . . . . . . 21 β„²π‘Žπ΅
3029, 14, 20cbviun 5001 . . . . . . . . . . . . . . . . . . . 20 βˆͺ π‘₯ ∈ 𝐴 𝐡 = βˆͺ π‘Ž ∈ 𝐴 β¦‹π‘Ž / π‘₯⦌𝐡
3128, 30sseqtrrdi 4000 . . . . . . . . . . . . . . . . . . 19 (π‘Ž ∈ 𝐴 β†’ β¦‹π‘Ž / π‘₯⦌𝐡 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡)
3231adantl 483 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ π‘Ž ∈ 𝐴) β†’ β¦‹π‘Ž / π‘₯⦌𝐡 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡)
3327, 32fssresd 6714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ π‘Ž ∈ 𝐴) β†’ (𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡):β¦‹π‘Ž / π‘₯β¦Œπ΅βŸΆβ„‚)
34 simpr 486 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ π‘Ž ∈ 𝐴) β†’ π‘Ž ∈ 𝐴)
35 limciun.2 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† β„‚)
3635ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ π‘Ž ∈ 𝐴) β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† β„‚)
37 nfcv 2908 . . . . . . . . . . . . . . . . . . . 20 β„²π‘₯β„‚
3814, 37nfss 3941 . . . . . . . . . . . . . . . . . . 19 β„²π‘₯β¦‹π‘Ž / π‘₯⦌𝐡 βŠ† β„‚
3920sseq1d 3980 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = π‘Ž β†’ (𝐡 βŠ† β„‚ ↔ β¦‹π‘Ž / π‘₯⦌𝐡 βŠ† β„‚))
4038, 39rspc 3572 . . . . . . . . . . . . . . . . . 18 (π‘Ž ∈ 𝐴 β†’ (βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† β„‚ β†’ β¦‹π‘Ž / π‘₯⦌𝐡 βŠ† β„‚))
4134, 36, 40sylc 65 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ π‘Ž ∈ 𝐴) β†’ β¦‹π‘Ž / π‘₯⦌𝐡 βŠ† β„‚)
42 limciun.4 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐢 ∈ β„‚)
4342ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ π‘Ž ∈ 𝐴) β†’ 𝐢 ∈ β„‚)
44 eqid 2737 . . . . . . . . . . . . . . . . 17 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
4533, 41, 43, 44ellimc2 25257 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ π‘Ž ∈ 𝐴) β†’ (𝑦 ∈ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) limβ„‚ 𝐢) ↔ (𝑦 ∈ β„‚ ∧ βˆ€π‘’ ∈ (TopOpenβ€˜β„‚fld)(𝑦 ∈ 𝑒 β†’ βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))))
4645adantlr 714 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ π‘Ž ∈ 𝐴) β†’ (𝑦 ∈ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) limβ„‚ 𝐢) ↔ (𝑦 ∈ β„‚ ∧ βˆ€π‘’ ∈ (TopOpenβ€˜β„‚fld)(𝑦 ∈ 𝑒 β†’ βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))))
4725, 46mpbid 231 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ π‘Ž ∈ 𝐴) β†’ (𝑦 ∈ β„‚ ∧ βˆ€π‘’ ∈ (TopOpenβ€˜β„‚fld)(𝑦 ∈ 𝑒 β†’ βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒))))
4847simprd 497 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ π‘Ž ∈ 𝐴) β†’ βˆ€π‘’ ∈ (TopOpenβ€˜β„‚fld)(𝑦 ∈ 𝑒 β†’ βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
49 simplrl 776 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ π‘Ž ∈ 𝐴) β†’ 𝑒 ∈ (TopOpenβ€˜β„‚fld))
50 simplrr 777 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ π‘Ž ∈ 𝐴) β†’ 𝑦 ∈ 𝑒)
51 rsp 3233 . . . . . . . . . . . . 13 (βˆ€π‘’ ∈ (TopOpenβ€˜β„‚fld)(𝑦 ∈ 𝑒 β†’ βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒)) β†’ (𝑒 ∈ (TopOpenβ€˜β„‚fld) β†’ (𝑦 ∈ 𝑒 β†’ βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒))))
5248, 49, 50, 51syl3c 66 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ π‘Ž ∈ 𝐴) β†’ βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
5352ralrimiva 3144 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) β†’ βˆ€π‘Ž ∈ 𝐴 βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
54 nfv 1918 . . . . . . . . . . . 12 β„²π‘Žβˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒)
55 nfcv 2908 . . . . . . . . . . . . 13 β„²π‘₯(TopOpenβ€˜β„‚fld)
56 nfv 1918 . . . . . . . . . . . . . 14 β„²π‘₯ 𝐢 ∈ π‘˜
57 nfcv 2908 . . . . . . . . . . . . . . . . 17 β„²π‘₯π‘˜
58 nfcv 2908 . . . . . . . . . . . . . . . . . 18 β„²π‘₯{𝐢}
5914, 58nfdif 4090 . . . . . . . . . . . . . . . . 17 β„²π‘₯(β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢})
6057, 59nfin 4181 . . . . . . . . . . . . . . . 16 β„²π‘₯(π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))
6115, 60nfima 6026 . . . . . . . . . . . . . . 15 β„²π‘₯((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢})))
62 nfcv 2908 . . . . . . . . . . . . . . 15 β„²π‘₯𝑒
6361, 62nfss 3941 . . . . . . . . . . . . . 14 β„²π‘₯((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒
6456, 63nfan 1903 . . . . . . . . . . . . 13 β„²π‘₯(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒)
6555, 64nfrexw 3299 . . . . . . . . . . . 12 β„²π‘₯βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒)
6620difeq1d 4086 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Ž β†’ (𝐡 βˆ– {𝐢}) = (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))
6766ineq2d 4177 . . . . . . . . . . . . . . . 16 (π‘₯ = π‘Ž β†’ (π‘˜ ∩ (𝐡 βˆ– {𝐢})) = (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢})))
6821, 67imaeq12d 6019 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ž β†’ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) = ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))))
6968sseq1d 3980 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ž β†’ (((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒 ↔ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
7069anbi2d 630 . . . . . . . . . . . . 13 (π‘₯ = π‘Ž β†’ ((𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒) ↔ (𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
7170rexbidv 3176 . . . . . . . . . . . 12 (π‘₯ = π‘Ž β†’ (βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒) ↔ βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
7254, 65, 71cbvralw 3292 . . . . . . . . . . 11 (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒) ↔ βˆ€π‘Ž ∈ 𝐴 βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ β¦‹π‘Ž / π‘₯⦌𝐡) β€œ (π‘˜ ∩ (β¦‹π‘Ž / π‘₯⦌𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
7353, 72sylibr 233 . . . . . . . . . 10 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) β†’ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
74 eleq2 2827 . . . . . . . . . . . 12 (π‘˜ = (π‘”β€˜π‘₯) β†’ (𝐢 ∈ π‘˜ ↔ 𝐢 ∈ (π‘”β€˜π‘₯)))
75 ineq1 4170 . . . . . . . . . . . . . 14 (π‘˜ = (π‘”β€˜π‘₯) β†’ (π‘˜ ∩ (𝐡 βˆ– {𝐢})) = ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢})))
7675imaeq2d 6018 . . . . . . . . . . . . 13 (π‘˜ = (π‘”β€˜π‘₯) β†’ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) = ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))))
7776sseq1d 3980 . . . . . . . . . . . 12 (π‘˜ = (π‘”β€˜π‘₯) β†’ (((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒 ↔ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
7874, 77anbi12d 632 . . . . . . . . . . 11 (π‘˜ = (π‘”β€˜π‘₯) β†’ ((𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒) ↔ (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
7978ac6sfi 9238 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘˜ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ π‘˜ ∧ ((𝐹 β†Ύ 𝐡) β€œ (π‘˜ ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒)) β†’ βˆƒπ‘”(𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
8011, 73, 79syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) β†’ βˆƒπ‘”(𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
8144cnfldtop 24163 . . . . . . . . . . 11 (TopOpenβ€˜β„‚fld) ∈ Top
82 frn 6680 . . . . . . . . . . . 12 (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) β†’ ran 𝑔 βŠ† (TopOpenβ€˜β„‚fld))
8382ad2antrl 727 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ ran 𝑔 βŠ† (TopOpenβ€˜β„‚fld))
8411adantr 482 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ 𝐴 ∈ Fin)
85 ffn 6673 . . . . . . . . . . . . . 14 (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) β†’ 𝑔 Fn 𝐴)
8685ad2antrl 727 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ 𝑔 Fn 𝐴)
87 dffn4 6767 . . . . . . . . . . . . 13 (𝑔 Fn 𝐴 ↔ 𝑔:𝐴–ontoβ†’ran 𝑔)
8886, 87sylib 217 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ 𝑔:𝐴–ontoβ†’ran 𝑔)
89 fofi 9289 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ 𝑔:𝐴–ontoβ†’ran 𝑔) β†’ ran 𝑔 ∈ Fin)
9084, 88, 89syl2anc 585 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ ran 𝑔 ∈ Fin)
91 unicntop 24165 . . . . . . . . . . . 12 β„‚ = βˆͺ (TopOpenβ€˜β„‚fld)
9291rintopn 22274 . . . . . . . . . . 11 (((TopOpenβ€˜β„‚fld) ∈ Top ∧ ran 𝑔 βŠ† (TopOpenβ€˜β„‚fld) ∧ ran 𝑔 ∈ Fin) β†’ (β„‚ ∩ ∩ ran 𝑔) ∈ (TopOpenβ€˜β„‚fld))
9381, 83, 90, 92mp3an2i 1467 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ (β„‚ ∩ ∩ ran 𝑔) ∈ (TopOpenβ€˜β„‚fld))
9442adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) β†’ 𝐢 ∈ β„‚)
9594ad2antrr 725 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ 𝐢 ∈ β„‚)
96 simpl 484 . . . . . . . . . . . . . 14 ((𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒) β†’ 𝐢 ∈ (π‘”β€˜π‘₯))
9796ralimi 3087 . . . . . . . . . . . . 13 (βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒) β†’ βˆ€π‘₯ ∈ 𝐴 𝐢 ∈ (π‘”β€˜π‘₯))
9897ad2antll 728 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ βˆ€π‘₯ ∈ 𝐴 𝐢 ∈ (π‘”β€˜π‘₯))
99 eleq2 2827 . . . . . . . . . . . . . 14 (𝑧 = (π‘”β€˜π‘₯) β†’ (𝐢 ∈ 𝑧 ↔ 𝐢 ∈ (π‘”β€˜π‘₯)))
10099ralrn 7043 . . . . . . . . . . . . 13 (𝑔 Fn 𝐴 β†’ (βˆ€π‘§ ∈ ran 𝑔 𝐢 ∈ 𝑧 ↔ βˆ€π‘₯ ∈ 𝐴 𝐢 ∈ (π‘”β€˜π‘₯)))
10186, 100syl 17 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ (βˆ€π‘§ ∈ ran 𝑔 𝐢 ∈ 𝑧 ↔ βˆ€π‘₯ ∈ 𝐴 𝐢 ∈ (π‘”β€˜π‘₯)))
10298, 101mpbird 257 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ βˆ€π‘§ ∈ ran 𝑔 𝐢 ∈ 𝑧)
103 elrint 4957 . . . . . . . . . . 11 (𝐢 ∈ (β„‚ ∩ ∩ ran 𝑔) ↔ (𝐢 ∈ β„‚ ∧ βˆ€π‘§ ∈ ran 𝑔 𝐢 ∈ 𝑧))
10495, 102, 103sylanbrc 584 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ 𝐢 ∈ (β„‚ ∩ ∩ ran 𝑔))
105 indifcom 4237 . . . . . . . . . . . . . 14 ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢})) = (βˆͺ π‘₯ ∈ 𝐴 𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))
106 iunin1 5037 . . . . . . . . . . . . . 14 βˆͺ π‘₯ ∈ 𝐴 (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢})) = (βˆͺ π‘₯ ∈ 𝐴 𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))
107105, 106eqtr4i 2768 . . . . . . . . . . . . 13 ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢})) = βˆͺ π‘₯ ∈ 𝐴 (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))
108107imaeq2i 6016 . . . . . . . . . . . 12 (𝐹 β€œ ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) = (𝐹 β€œ βˆͺ π‘₯ ∈ 𝐴 (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢})))
109 imaiun 7197 . . . . . . . . . . . 12 (𝐹 β€œ βˆͺ π‘₯ ∈ 𝐴 (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) = βˆͺ π‘₯ ∈ 𝐴 (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢})))
110108, 109eqtri 2765 . . . . . . . . . . 11 (𝐹 β€œ ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) = βˆͺ π‘₯ ∈ 𝐴 (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢})))
111 inss2 4194 . . . . . . . . . . . . . . . . . . . . 21 (β„‚ ∩ ∩ ran 𝑔) βŠ† ∩ ran 𝑔
112 fnfvelrn 7036 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 Fn 𝐴 ∧ π‘₯ ∈ 𝐴) β†’ (π‘”β€˜π‘₯) ∈ ran 𝑔)
11385, 112sylan 581 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ π‘₯ ∈ 𝐴) β†’ (π‘”β€˜π‘₯) ∈ ran 𝑔)
114 intss1 4929 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘”β€˜π‘₯) ∈ ran 𝑔 β†’ ∩ ran 𝑔 βŠ† (π‘”β€˜π‘₯))
115113, 114syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ π‘₯ ∈ 𝐴) β†’ ∩ ran 𝑔 βŠ† (π‘”β€˜π‘₯))
116111, 115sstrid 3960 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ π‘₯ ∈ 𝐴) β†’ (β„‚ ∩ ∩ ran 𝑔) βŠ† (π‘”β€˜π‘₯))
117116ssdifd 4105 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ π‘₯ ∈ 𝐴) β†’ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}) βŠ† ((π‘”β€˜π‘₯) βˆ– {𝐢}))
118 sslin 4199 . . . . . . . . . . . . . . . . . . 19 (((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}) βŠ† ((π‘”β€˜π‘₯) βˆ– {𝐢}) β†’ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢})) βŠ† (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢})))
119 imass2 6059 . . . . . . . . . . . . . . . . . . 19 ((𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢})) βŠ† (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢})) β†’ (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† (𝐹 β€œ (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢}))))
120117, 118, 1193syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ π‘₯ ∈ 𝐴) β†’ (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† (𝐹 β€œ (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢}))))
121 indifcom 4237 . . . . . . . . . . . . . . . . . . . 20 ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢})) = (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢}))
122121imaeq2i 6016 . . . . . . . . . . . . . . . . . . 19 ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) = ((𝐹 β†Ύ 𝐡) β€œ (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢})))
123 inss1 4193 . . . . . . . . . . . . . . . . . . . 20 (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢})) βŠ† 𝐡
124 resima2 5977 . . . . . . . . . . . . . . . . . . . 20 ((𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢})) βŠ† 𝐡 β†’ ((𝐹 β†Ύ 𝐡) β€œ (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢}))) = (𝐹 β€œ (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢}))))
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝐹 β†Ύ 𝐡) β€œ (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢}))) = (𝐹 β€œ (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢})))
126122, 125eqtri 2765 . . . . . . . . . . . . . . . . . 18 ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) = (𝐹 β€œ (𝐡 ∩ ((π‘”β€˜π‘₯) βˆ– {𝐢})))
127120, 126sseqtrrdi 4000 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ π‘₯ ∈ 𝐴) β†’ (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))))
128 sstr2 3956 . . . . . . . . . . . . . . . . 17 ((𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) β†’ (((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒 β†’ (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒))
129127, 128syl 17 . . . . . . . . . . . . . . . 16 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ π‘₯ ∈ 𝐴) β†’ (((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒 β†’ (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒))
130129adantld 492 . . . . . . . . . . . . . . 15 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ π‘₯ ∈ 𝐴) β†’ ((𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒) β†’ (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒))
131130ralimdva 3165 . . . . . . . . . . . . . 14 (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) β†’ (βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒) β†’ βˆ€π‘₯ ∈ 𝐴 (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒))
132131imp 408 . . . . . . . . . . . . 13 ((𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒)) β†’ βˆ€π‘₯ ∈ 𝐴 (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒)
133132adantl 483 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ βˆ€π‘₯ ∈ 𝐴 (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒)
134 iunss 5010 . . . . . . . . . . . 12 (βˆͺ π‘₯ ∈ 𝐴 (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒 ↔ βˆ€π‘₯ ∈ 𝐴 (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒)
135133, 134sylibr 233 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ βˆͺ π‘₯ ∈ 𝐴 (𝐹 β€œ (𝐡 ∩ ((β„‚ ∩ ∩ ran 𝑔) βˆ– {𝐢}))) βŠ† 𝑒)
136110, 135eqsstrid 3997 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ (𝐹 β€œ ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒)
137 eleq2 2827 . . . . . . . . . . . 12 (𝑣 = (β„‚ ∩ ∩ ran 𝑔) β†’ (𝐢 ∈ 𝑣 ↔ 𝐢 ∈ (β„‚ ∩ ∩ ran 𝑔)))
138 ineq1 4170 . . . . . . . . . . . . . 14 (𝑣 = (β„‚ ∩ ∩ ran 𝑔) β†’ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢})) = ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢})))
139138imaeq2d 6018 . . . . . . . . . . . . 13 (𝑣 = (β„‚ ∩ ∩ ran 𝑔) β†’ (𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) = (𝐹 β€œ ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))))
140139sseq1d 3980 . . . . . . . . . . . 12 (𝑣 = (β„‚ ∩ ∩ ran 𝑔) β†’ ((𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒 ↔ (𝐹 β€œ ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
141137, 140anbi12d 632 . . . . . . . . . . 11 (𝑣 = (β„‚ ∩ ∩ ran 𝑔) β†’ ((𝐢 ∈ 𝑣 ∧ (𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒) ↔ (𝐢 ∈ (β„‚ ∩ ∩ ran 𝑔) ∧ (𝐹 β€œ ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
142141rspcev 3584 . . . . . . . . . 10 (((β„‚ ∩ ∩ ran 𝑔) ∈ (TopOpenβ€˜β„‚fld) ∧ (𝐢 ∈ (β„‚ ∩ ∩ ran 𝑔) ∧ (𝐹 β€œ ((β„‚ ∩ ∩ ran 𝑔) ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒)) β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ 𝑣 ∧ (𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
14393, 104, 136, 142syl12anc 836 . . . . . . . . 9 ((((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) ∧ (𝑔:𝐴⟢(TopOpenβ€˜β„‚fld) ∧ βˆ€π‘₯ ∈ 𝐴 (𝐢 ∈ (π‘”β€˜π‘₯) ∧ ((𝐹 β†Ύ 𝐡) β€œ ((π‘”β€˜π‘₯) ∩ (𝐡 βˆ– {𝐢}))) βŠ† 𝑒))) β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ 𝑣 ∧ (𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
14480, 143exlimddv 1939 . . . . . . . 8 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ (𝑒 ∈ (TopOpenβ€˜β„‚fld) ∧ 𝑦 ∈ 𝑒)) β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ 𝑣 ∧ (𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒))
145144expr 458 . . . . . . 7 (((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) ∧ 𝑒 ∈ (TopOpenβ€˜β„‚fld)) β†’ (𝑦 ∈ 𝑒 β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ 𝑣 ∧ (𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
146145ralrimiva 3144 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) β†’ βˆ€π‘’ ∈ (TopOpenβ€˜β„‚fld)(𝑦 ∈ 𝑒 β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ 𝑣 ∧ (𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))
14726adantr 482 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) β†’ 𝐹:βˆͺ π‘₯ ∈ 𝐴 π΅βŸΆβ„‚)
148 iunss 5010 . . . . . . . . 9 (βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† β„‚ ↔ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† β„‚)
14935, 148sylibr 233 . . . . . . . 8 (πœ‘ β†’ βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† β„‚)
150149adantr 482 . . . . . . 7 ((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) β†’ βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† β„‚)
151147, 150, 94, 44ellimc2 25257 . . . . . 6 ((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) β†’ (𝑦 ∈ (𝐹 limβ„‚ 𝐢) ↔ (𝑦 ∈ β„‚ ∧ βˆ€π‘’ ∈ (TopOpenβ€˜β„‚fld)(𝑦 ∈ 𝑒 β†’ βˆƒπ‘£ ∈ (TopOpenβ€˜β„‚fld)(𝐢 ∈ 𝑣 ∧ (𝐹 β€œ (𝑣 ∩ (βˆͺ π‘₯ ∈ 𝐴 𝐡 βˆ– {𝐢}))) βŠ† 𝑒)))))
1529, 146, 151mpbir2and 712 . . . . 5 ((πœ‘ ∧ (𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢))) β†’ 𝑦 ∈ (𝐹 limβ„‚ 𝐢))
153152ex 414 . . . 4 (πœ‘ β†’ ((𝑦 ∈ β„‚ ∧ βˆ€π‘₯ ∈ 𝐴 𝑦 ∈ ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)) β†’ 𝑦 ∈ (𝐹 limβ„‚ 𝐢)))
1548, 153biimtrid 241 . . 3 (πœ‘ β†’ (𝑦 ∈ (β„‚ ∩ ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)) β†’ 𝑦 ∈ (𝐹 limβ„‚ 𝐢)))
155154ssrdv 3955 . 2 (πœ‘ β†’ (β„‚ ∩ ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)) βŠ† (𝐹 limβ„‚ 𝐢))
1567, 155eqssd 3966 1 (πœ‘ β†’ (𝐹 limβ„‚ 𝐢) = (β„‚ ∩ ∩ π‘₯ ∈ 𝐴 ((𝐹 β†Ύ 𝐡) limβ„‚ 𝐢)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3065  βˆƒwrex 3074  β¦‹csb 3860   βˆ– cdif 3912   ∩ cin 3914   βŠ† wss 3915  {csn 4591  βˆ© cint 4912  βˆͺ ciun 4959  βˆ© ciin 4960  ran crn 5639   β†Ύ cres 5640   β€œ cima 5641   Fn wfn 6496  βŸΆwf 6497  β€“ontoβ†’wfo 6499  β€˜cfv 6501  (class class class)co 7362  Fincfn 8890  β„‚cc 11056  TopOpenctopn 17310  β„‚fldccnfld 20812  Topctop 22258   limβ„‚ climc 25242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fi 9354  df-sup 9385  df-inf 9386  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-fz 13432  df-seq 13914  df-exp 13975  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-struct 17026  df-slot 17061  df-ndx 17073  df-base 17091  df-plusg 17153  df-mulr 17154  df-starv 17155  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-rest 17311  df-topn 17312  df-topgen 17332  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cnp 22595  df-xms 23689  df-ms 23690  df-limc 25246
This theorem is referenced by:  limcun  25275
  Copyright terms: Public domain W3C validator