ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tgcnp GIF version
Theorem tgcnp 13712
Description: The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
tgcn.1 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
tgcn.3 (πœ‘ β†’ 𝐾 = (topGenβ€˜π΅))
tgcn.4 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
tgcnp.5 (πœ‘ β†’ 𝑃 ∈ 𝑋)
Assertion
Ref Expression
tgcnp (πœ‘ β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
Distinct variable groups:   π‘₯,𝑦,𝐡   π‘₯,𝐹,𝑦   π‘₯,𝐽,𝑦   π‘₯,𝐾,𝑦   π‘₯,𝑃,𝑦   πœ‘,π‘₯   π‘₯,𝑋,𝑦   π‘₯,π‘Œ,𝑦
Allowed substitution hint:   πœ‘(𝑦)
Proof of Theorem tgcnp
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 tgcn.1 . . . 4 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
2 tgcn.4 . . . 4 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
3 tgcnp.5 . . . 4 (πœ‘ β†’ 𝑃 ∈ 𝑋)
4 iscnp 13702 . . . 4 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑃 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
51, 2, 3, 4syl3anc 1238 . . 3 (πœ‘ β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
6 tgcn.3 . . . . . . . . 9 (πœ‘ β†’ 𝐾 = (topGenβ€˜π΅))
7 topontop 13517 . . . . . . . . . 10 (𝐾 ∈ (TopOnβ€˜π‘Œ) β†’ 𝐾 ∈ Top)
82, 7syl 14 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ Top)
96, 8eqeltrrd 2255 . . . . . . . 8 (πœ‘ β†’ (topGenβ€˜π΅) ∈ Top)
10 tgclb 13568 . . . . . . . 8 (𝐡 ∈ TopBases ↔ (topGenβ€˜π΅) ∈ Top)
119, 10sylibr 134 . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ TopBases)
12 bastg 13564 . . . . . . 7 (𝐡 ∈ TopBases β†’ 𝐡 βŠ† (topGenβ€˜π΅))
1311, 12syl 14 . . . . . 6 (πœ‘ β†’ 𝐡 βŠ† (topGenβ€˜π΅))
1413, 6sseqtrrd 3195 . . . . 5 (πœ‘ β†’ 𝐡 βŠ† 𝐾)
15 ssralv 3220 . . . . 5 (𝐡 βŠ† 𝐾 β†’ (βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦))))
1614, 15syl 14 . . . 4 (πœ‘ β†’ (βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦))))
1716anim2d 337 . . 3 (πœ‘ β†’ ((𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦))) β†’ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
185, 17sylbid 150 . 2 (πœ‘ β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
196eleq2d 2247 . . . . . . 7 (πœ‘ β†’ (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ (topGenβ€˜π΅)))
2019biimpa 296 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐾) β†’ 𝑧 ∈ (topGenβ€˜π΅))
21 tg2 13563 . . . . . . . . 9 ((𝑧 ∈ (topGenβ€˜π΅) ∧ (πΉβ€˜π‘ƒ) ∈ 𝑧) β†’ βˆƒπ‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ 𝑦 βŠ† 𝑧))
22 r19.29 2614 . . . . . . . . . . 11 ((βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) ∧ βˆƒπ‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ 𝑦 βŠ† 𝑧)) β†’ βˆƒπ‘¦ ∈ 𝐡 (((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ 𝑦 βŠ† 𝑧)))
23 sstr 3164 . . . . . . . . . . . . . . . . . 18 (((𝐹 β€œ π‘₯) βŠ† 𝑦 ∧ 𝑦 βŠ† 𝑧) β†’ (𝐹 β€œ π‘₯) βŠ† 𝑧)
2423expcom 116 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† 𝑧 β†’ ((𝐹 β€œ π‘₯) βŠ† 𝑦 β†’ (𝐹 β€œ π‘₯) βŠ† 𝑧))
2524anim2d 337 . . . . . . . . . . . . . . . 16 (𝑦 βŠ† 𝑧 β†’ ((𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦) β†’ (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧)))
2625reximdv 2578 . . . . . . . . . . . . . . 15 (𝑦 βŠ† 𝑧 β†’ (βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧)))
2726com12 30 . . . . . . . . . . . . . 14 (βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦) β†’ (𝑦 βŠ† 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧)))
2827imim2i 12 . . . . . . . . . . . . 13 (((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ (𝑦 βŠ† 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧))))
2928imp32 257 . . . . . . . . . . . 12 ((((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ 𝑦 βŠ† 𝑧)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧))
3029rexlimivw 2590 . . . . . . . . . . 11 (βˆƒπ‘¦ ∈ 𝐡 (((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) ∧ ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ 𝑦 βŠ† 𝑧)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧))
3122, 30syl 14 . . . . . . . . . 10 ((βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) ∧ βˆƒπ‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ 𝑦 βŠ† 𝑧)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧))
3231expcom 116 . . . . . . . . 9 (βˆƒπ‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 ∧ 𝑦 βŠ† 𝑧) β†’ (βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧)))
3321, 32syl 14 . . . . . . . 8 ((𝑧 ∈ (topGenβ€˜π΅) ∧ (πΉβ€˜π‘ƒ) ∈ 𝑧) β†’ (βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧)))
3433ex 115 . . . . . . 7 (𝑧 ∈ (topGenβ€˜π΅) β†’ ((πΉβ€˜π‘ƒ) ∈ 𝑧 β†’ (βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧))))
3534com23 78 . . . . . 6 (𝑧 ∈ (topGenβ€˜π΅) β†’ (βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ ((πΉβ€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧))))
3620, 35syl 14 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝐾) β†’ (βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ ((πΉβ€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧))))
3736ralrimdva 2557 . . . 4 (πœ‘ β†’ (βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)) β†’ βˆ€π‘§ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧))))
3837anim2d 337 . . 3 (πœ‘ β†’ ((𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦))) β†’ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘§ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧)))))
39 iscnp 13702 . . . 4 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑃 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘§ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧)))))
401, 2, 3, 39syl3anc 1238 . . 3 (πœ‘ β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘§ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑧 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑧)))))
4138, 40sylibrd 169 . 2 (πœ‘ β†’ ((𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦))) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)))
4218, 41impbid 129 1 (πœ‘ β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455  βˆƒwrex 2456   βŠ† wss 3130   β€œ cima 4630  βŸΆwf 5213  β€˜cfv 5217  (class class class)co 5875  topGenctg 12703  Topctop 13500  TopOnctopon 13513  TopBasesctb 13545   CnP ccnp 13689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-map 6650  df-topgen 12709  df-top 13501  df-topon 13514  df-bases 13546  df-cnp 13692
This theorem is referenced by:  txcnp  13774  metcnp3  14014
  Copyright terms: Public domain W3C validator