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

Theorem lmss 23189
Description: Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
Hypotheses
Ref Expression
lmss.1 𝐾 = (𝐽 β†Ύt π‘Œ)
lmss.2 𝑍 = (β„€β‰₯β€˜π‘€)
lmss.3 (πœ‘ β†’ π‘Œ ∈ 𝑉)
lmss.4 (πœ‘ β†’ 𝐽 ∈ Top)
lmss.5 (πœ‘ β†’ 𝑃 ∈ π‘Œ)
lmss.6 (πœ‘ β†’ 𝑀 ∈ β„€)
lmss.7 (πœ‘ β†’ 𝐹:π‘βŸΆπ‘Œ)
Assertion
Ref Expression
lmss (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ 𝐹(β‡π‘‘β€˜πΎ)𝑃))

Proof of Theorem lmss
Dummy variables 𝑗 π‘˜ 𝑒 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmss.4 . . . . . 6 (πœ‘ β†’ 𝐽 ∈ Top)
2 toptopon2 22807 . . . . . 6 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽))
31, 2sylib 217 . . . . 5 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽))
4 lmcl 23188 . . . . 5 ((𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽) ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ 𝑃 ∈ βˆͺ 𝐽)
53, 4sylan 579 . . . 4 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ 𝑃 ∈ βˆͺ 𝐽)
6 lmfss 23187 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽) ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ 𝐹 βŠ† (β„‚ Γ— βˆͺ 𝐽))
73, 6sylan 579 . . . . . 6 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ 𝐹 βŠ† (β„‚ Γ— βˆͺ 𝐽))
8 rnss 5935 . . . . . 6 (𝐹 βŠ† (β„‚ Γ— βˆͺ 𝐽) β†’ ran 𝐹 βŠ† ran (β„‚ Γ— βˆͺ 𝐽))
97, 8syl 17 . . . . 5 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ ran 𝐹 βŠ† ran (β„‚ Γ— βˆͺ 𝐽))
10 rnxpss 6170 . . . . 5 ran (β„‚ Γ— βˆͺ 𝐽) βŠ† βˆͺ 𝐽
119, 10sstrdi 3990 . . . 4 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ ran 𝐹 βŠ† βˆͺ 𝐽)
125, 11jca 511 . . 3 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽))
1312ex 412 . 2 (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 β†’ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)))
14 lmss.1 . . . . . . 7 𝐾 = (𝐽 β†Ύt π‘Œ)
15 lmss.3 . . . . . . . 8 (πœ‘ β†’ π‘Œ ∈ 𝑉)
16 resttopon2 23059 . . . . . . . 8 ((𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽) ∧ π‘Œ ∈ 𝑉) β†’ (𝐽 β†Ύt π‘Œ) ∈ (TopOnβ€˜(π‘Œ ∩ βˆͺ 𝐽)))
173, 15, 16syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐽 β†Ύt π‘Œ) ∈ (TopOnβ€˜(π‘Œ ∩ βˆͺ 𝐽)))
1814, 17eqeltrid 2832 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜(π‘Œ ∩ βˆͺ 𝐽)))
19 lmcl 23188 . . . . . 6 ((𝐾 ∈ (TopOnβ€˜(π‘Œ ∩ βˆͺ 𝐽)) ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ 𝑃 ∈ (π‘Œ ∩ βˆͺ 𝐽))
2018, 19sylan 579 . . . . 5 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ 𝑃 ∈ (π‘Œ ∩ βˆͺ 𝐽))
2120elin2d 4195 . . . 4 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ 𝑃 ∈ βˆͺ 𝐽)
22 lmfss 23187 . . . . . . . 8 ((𝐾 ∈ (TopOnβ€˜(π‘Œ ∩ βˆͺ 𝐽)) ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ 𝐹 βŠ† (β„‚ Γ— (π‘Œ ∩ βˆͺ 𝐽)))
2318, 22sylan 579 . . . . . . 7 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ 𝐹 βŠ† (β„‚ Γ— (π‘Œ ∩ βˆͺ 𝐽)))
24 rnss 5935 . . . . . . 7 (𝐹 βŠ† (β„‚ Γ— (π‘Œ ∩ βˆͺ 𝐽)) β†’ ran 𝐹 βŠ† ran (β„‚ Γ— (π‘Œ ∩ βˆͺ 𝐽)))
2523, 24syl 17 . . . . . 6 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ ran 𝐹 βŠ† ran (β„‚ Γ— (π‘Œ ∩ βˆͺ 𝐽)))
26 rnxpss 6170 . . . . . 6 ran (β„‚ Γ— (π‘Œ ∩ βˆͺ 𝐽)) βŠ† (π‘Œ ∩ βˆͺ 𝐽)
2725, 26sstrdi 3990 . . . . 5 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ ran 𝐹 βŠ† (π‘Œ ∩ βˆͺ 𝐽))
28 inss2 4225 . . . . 5 (π‘Œ ∩ βˆͺ 𝐽) βŠ† βˆͺ 𝐽
2927, 28sstrdi 3990 . . . 4 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ ran 𝐹 βŠ† βˆͺ 𝐽)
3021, 29jca 511 . . 3 ((πœ‘ ∧ 𝐹(β‡π‘‘β€˜πΎ)𝑃) β†’ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽))
3130ex 412 . 2 (πœ‘ β†’ (𝐹(β‡π‘‘β€˜πΎ)𝑃 β†’ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)))
32 simprl 770 . . . . . 6 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝑃 ∈ βˆͺ 𝐽)
33 lmss.5 . . . . . . . 8 (πœ‘ β†’ 𝑃 ∈ π‘Œ)
3433adantr 480 . . . . . . 7 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝑃 ∈ π‘Œ)
3534, 32elind 4190 . . . . . 6 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝑃 ∈ (π‘Œ ∩ βˆͺ 𝐽))
3632, 352thd 265 . . . . 5 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (𝑃 ∈ βˆͺ 𝐽 ↔ 𝑃 ∈ (π‘Œ ∩ βˆͺ 𝐽)))
3714eleq2i 2820 . . . . . . . . 9 (𝑣 ∈ 𝐾 ↔ 𝑣 ∈ (𝐽 β†Ύt π‘Œ))
381adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝐽 ∈ Top)
3915adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ π‘Œ ∈ 𝑉)
40 elrest 17400 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ π‘Œ ∈ 𝑉) β†’ (𝑣 ∈ (𝐽 β†Ύt π‘Œ) ↔ βˆƒπ‘’ ∈ 𝐽 𝑣 = (𝑒 ∩ π‘Œ)))
4138, 39, 40syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (𝑣 ∈ (𝐽 β†Ύt π‘Œ) ↔ βˆƒπ‘’ ∈ 𝐽 𝑣 = (𝑒 ∩ π‘Œ)))
4241biimpa 476 . . . . . . . . 9 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑣 ∈ (𝐽 β†Ύt π‘Œ)) β†’ βˆƒπ‘’ ∈ 𝐽 𝑣 = (𝑒 ∩ π‘Œ))
4337, 42sylan2b 593 . . . . . . . 8 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑣 ∈ 𝐾) β†’ βˆƒπ‘’ ∈ 𝐽 𝑣 = (𝑒 ∩ π‘Œ))
44 r19.29r 3111 . . . . . . . . . 10 ((βˆƒπ‘’ ∈ 𝐽 𝑣 = (𝑒 ∩ π‘Œ) ∧ βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒)) β†’ βˆƒπ‘’ ∈ 𝐽 (𝑣 = (𝑒 ∩ π‘Œ) ∧ (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒)))
4534biantrud 531 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (𝑃 ∈ 𝑒 ↔ (𝑃 ∈ 𝑒 ∧ 𝑃 ∈ π‘Œ)))
46 elin 3960 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (𝑒 ∩ π‘Œ) ↔ (𝑃 ∈ 𝑒 ∧ 𝑃 ∈ π‘Œ))
4745, 46bitr4di 289 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (𝑃 ∈ 𝑒 ↔ 𝑃 ∈ (𝑒 ∩ π‘Œ)))
48 lmss.2 . . . . . . . . . . . . . . . . . . . . 21 𝑍 = (β„€β‰₯β€˜π‘€)
4948uztrn2 12863 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ 𝑍 ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ π‘˜ ∈ 𝑍)
50 lmss.7 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝐹:π‘βŸΆπ‘Œ)
5150adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝐹:π‘βŸΆπ‘Œ)
5251ffvelcdmda 7088 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ π‘˜ ∈ 𝑍) β†’ (πΉβ€˜π‘˜) ∈ π‘Œ)
5352biantrud 531 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ π‘˜ ∈ 𝑍) β†’ ((πΉβ€˜π‘˜) ∈ 𝑒 ↔ ((πΉβ€˜π‘˜) ∈ 𝑒 ∧ (πΉβ€˜π‘˜) ∈ π‘Œ)))
54 elin 3960 . . . . . . . . . . . . . . . . . . . . 21 ((πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ) ↔ ((πΉβ€˜π‘˜) ∈ 𝑒 ∧ (πΉβ€˜π‘˜) ∈ π‘Œ))
5553, 54bitr4di 289 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ π‘˜ ∈ 𝑍) β†’ ((πΉβ€˜π‘˜) ∈ 𝑒 ↔ (πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ)))
5649, 55sylan2 592 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ (𝑗 ∈ 𝑍 ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—))) β†’ ((πΉβ€˜π‘˜) ∈ 𝑒 ↔ (πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ)))
5756anassrs 467 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑗 ∈ 𝑍) ∧ π‘˜ ∈ (β„€β‰₯β€˜π‘—)) β†’ ((πΉβ€˜π‘˜) ∈ 𝑒 ↔ (πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ)))
5857ralbidva 3170 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑗 ∈ 𝑍) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒 ↔ βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ)))
5958rexbidva 3171 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒 ↔ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ)))
6047, 59imbi12d 344 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ ((𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) ↔ (𝑃 ∈ (𝑒 ∩ π‘Œ) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ))))
6160adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ ((𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) ↔ (𝑃 ∈ (𝑒 ∩ π‘Œ) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ))))
6261biimpd 228 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ ((𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) β†’ (𝑃 ∈ (𝑒 ∩ π‘Œ) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ))))
63 eleq2 2817 . . . . . . . . . . . . . . 15 (𝑣 = (𝑒 ∩ π‘Œ) β†’ (𝑃 ∈ 𝑣 ↔ 𝑃 ∈ (𝑒 ∩ π‘Œ)))
64 eleq2 2817 . . . . . . . . . . . . . . . 16 (𝑣 = (𝑒 ∩ π‘Œ) β†’ ((πΉβ€˜π‘˜) ∈ 𝑣 ↔ (πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ)))
6564rexralbidv 3215 . . . . . . . . . . . . . . 15 (𝑣 = (𝑒 ∩ π‘Œ) β†’ (βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣 ↔ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ)))
6663, 65imbi12d 344 . . . . . . . . . . . . . 14 (𝑣 = (𝑒 ∩ π‘Œ) β†’ ((𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣) ↔ (𝑃 ∈ (𝑒 ∩ π‘Œ) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ))))
6766imbi2d 340 . . . . . . . . . . . . 13 (𝑣 = (𝑒 ∩ π‘Œ) β†’ (((𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) β†’ (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣)) ↔ ((𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) β†’ (𝑃 ∈ (𝑒 ∩ π‘Œ) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ)))))
6862, 67syl5ibrcom 246 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ (𝑣 = (𝑒 ∩ π‘Œ) β†’ ((𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) β†’ (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣))))
6968impd 410 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ ((𝑣 = (𝑒 ∩ π‘Œ) ∧ (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒)) β†’ (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣)))
7069rexlimdva 3150 . . . . . . . . . 10 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (βˆƒπ‘’ ∈ 𝐽 (𝑣 = (𝑒 ∩ π‘Œ) ∧ (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒)) β†’ (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣)))
7144, 70syl5 34 . . . . . . . . 9 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ ((βˆƒπ‘’ ∈ 𝐽 𝑣 = (𝑒 ∩ π‘Œ) ∧ βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒)) β†’ (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣)))
7271expdimp 452 . . . . . . . 8 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ βˆƒπ‘’ ∈ 𝐽 𝑣 = (𝑒 ∩ π‘Œ)) β†’ (βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) β†’ (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣)))
7343, 72syldan 590 . . . . . . 7 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑣 ∈ 𝐾) β†’ (βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) β†’ (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣)))
7473ralrimdva 3149 . . . . . 6 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) β†’ βˆ€π‘£ ∈ 𝐾 (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣)))
7538adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ 𝐽 ∈ Top)
7639adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ π‘Œ ∈ 𝑉)
77 simpr 484 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ 𝑒 ∈ 𝐽)
78 elrestr 17401 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ π‘Œ ∈ 𝑉 ∧ 𝑒 ∈ 𝐽) β†’ (𝑒 ∩ π‘Œ) ∈ (𝐽 β†Ύt π‘Œ))
7975, 76, 77, 78syl3anc 1369 . . . . . . . . . 10 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ (𝑒 ∩ π‘Œ) ∈ (𝐽 β†Ύt π‘Œ))
8079, 14eleqtrrdi 2839 . . . . . . . . 9 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ (𝑒 ∩ π‘Œ) ∈ 𝐾)
8166rspcv 3603 . . . . . . . . 9 ((𝑒 ∩ π‘Œ) ∈ 𝐾 β†’ (βˆ€π‘£ ∈ 𝐾 (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣) β†’ (𝑃 ∈ (𝑒 ∩ π‘Œ) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ))))
8280, 81syl 17 . . . . . . . 8 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ (βˆ€π‘£ ∈ 𝐾 (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣) β†’ (𝑃 ∈ (𝑒 ∩ π‘Œ) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ (𝑒 ∩ π‘Œ))))
8382, 61sylibrd 259 . . . . . . 7 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ 𝑒 ∈ 𝐽) β†’ (βˆ€π‘£ ∈ 𝐾 (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣) β†’ (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒)))
8483ralrimdva 3149 . . . . . 6 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (βˆ€π‘£ ∈ 𝐾 (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣) β†’ βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒)))
8574, 84impbid 211 . . . . 5 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒) ↔ βˆ€π‘£ ∈ 𝐾 (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣)))
8636, 85anbi12d 630 . . . 4 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ ((𝑃 ∈ βˆͺ 𝐽 ∧ βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒)) ↔ (𝑃 ∈ (π‘Œ ∩ βˆͺ 𝐽) ∧ βˆ€π‘£ ∈ 𝐾 (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣))))
8738, 2sylib 217 . . . . 5 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝐽 ∈ (TopOnβ€˜βˆͺ 𝐽))
88 lmss.6 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„€)
8988adantr 480 . . . . 5 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝑀 ∈ β„€)
9051ffnd 6717 . . . . . 6 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝐹 Fn 𝑍)
91 simprr 772 . . . . . 6 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ ran 𝐹 βŠ† βˆͺ 𝐽)
92 df-f 6546 . . . . . 6 (𝐹:π‘βŸΆβˆͺ 𝐽 ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 βŠ† βˆͺ 𝐽))
9390, 91, 92sylanbrc 582 . . . . 5 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝐹:π‘βŸΆβˆͺ 𝐽)
94 eqidd 2728 . . . . 5 (((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) ∧ π‘˜ ∈ 𝑍) β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘˜))
9587, 48, 89, 93, 94lmbrf 23151 . . . 4 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ (𝑃 ∈ βˆͺ 𝐽 ∧ βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑒))))
9618adantr 480 . . . . 5 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝐾 ∈ (TopOnβ€˜(π‘Œ ∩ βˆͺ 𝐽)))
9751frnd 6724 . . . . . . 7 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ ran 𝐹 βŠ† π‘Œ)
9897, 91ssind 4228 . . . . . 6 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ ran 𝐹 βŠ† (π‘Œ ∩ βˆͺ 𝐽))
99 df-f 6546 . . . . . 6 (𝐹:π‘βŸΆ(π‘Œ ∩ βˆͺ 𝐽) ↔ (𝐹 Fn 𝑍 ∧ ran 𝐹 βŠ† (π‘Œ ∩ βˆͺ 𝐽)))
10090, 98, 99sylanbrc 582 . . . . 5 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ 𝐹:π‘βŸΆ(π‘Œ ∩ βˆͺ 𝐽))
10196, 48, 89, 100, 94lmbrf 23151 . . . 4 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (𝐹(β‡π‘‘β€˜πΎ)𝑃 ↔ (𝑃 ∈ (π‘Œ ∩ βˆͺ 𝐽) ∧ βˆ€π‘£ ∈ 𝐾 (𝑃 ∈ 𝑣 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ 𝑣))))
10286, 95, 1013bitr4d 311 . . 3 ((πœ‘ ∧ (𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽)) β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ 𝐹(β‡π‘‘β€˜πΎ)𝑃))
103102ex 412 . 2 (πœ‘ β†’ ((𝑃 ∈ βˆͺ 𝐽 ∧ ran 𝐹 βŠ† βˆͺ 𝐽) β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ 𝐹(β‡π‘‘β€˜πΎ)𝑃)))
10413, 31, 103pm5.21ndd 379 1 (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ 𝐹(β‡π‘‘β€˜πΎ)𝑃))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  βˆ€wral 3056  βˆƒwrex 3065   ∩ cin 3943   βŠ† wss 3944  βˆͺ cuni 4903   class class class wbr 5142   Γ— cxp 5670  ran crn 5673   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414  β„‚cc 11128  β„€cz 12580  β„€β‰₯cuz 12844   β†Ύt crest 17393  Topctop 22782  TopOnctopon 22799  β‡π‘‘clm 23117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-pre-lttri 11204  ax-pre-lttrn 11205
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-er 8718  df-pm 8839  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fi 9426  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-neg 11469  df-z 12581  df-uz 12845  df-rest 17395  df-topgen 17416  df-top 22783  df-topon 22800  df-bases 22836  df-lm 23120
This theorem is referenced by:  1stckgen  23445  minvecolem4b  30675  minvecolem4  30677  hhsscms  31075  lmlim  33484  climreeq  44924  xlimclim  45135
  Copyright terms: Public domain W3C validator