ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnpdis GIF version

Theorem cnpdis 12842
Description: If 𝐴 is an isolated point in 𝑋 (or equivalently, the singleton {𝐴} is open in 𝑋), then every function is continuous at 𝐴. (Contributed by Mario Carneiro, 9-Sep-2015.)
Assertion
Ref Expression
cnpdis (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → ((𝐽 CnP 𝐾)‘𝐴) = (𝑌𝑚 𝑋))

Proof of Theorem cnpdis
Dummy variables 𝑥 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplrl 525 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → {𝐴} ∈ 𝐽)
2 simpll3 1028 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → 𝐴𝑋)
3 snidg 3604 . . . . . . . . 9 (𝐴𝑋𝐴 ∈ {𝐴})
42, 3syl 14 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → 𝐴 ∈ {𝐴})
5 simprr 522 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → (𝑓𝐴) ∈ 𝑥)
6 simplrr 526 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → 𝑓:𝑋𝑌)
7 ffn 5336 . . . . . . . . . . 11 (𝑓:𝑋𝑌𝑓 Fn 𝑋)
8 elpreima 5603 . . . . . . . . . . 11 (𝑓 Fn 𝑋 → (𝐴 ∈ (𝑓𝑥) ↔ (𝐴𝑋 ∧ (𝑓𝐴) ∈ 𝑥)))
96, 7, 83syl 17 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → (𝐴 ∈ (𝑓𝑥) ↔ (𝐴𝑋 ∧ (𝑓𝐴) ∈ 𝑥)))
102, 5, 9mpbir2and 934 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → 𝐴 ∈ (𝑓𝑥))
1110snssd 3717 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → {𝐴} ⊆ (𝑓𝑥))
12 eleq2 2229 . . . . . . . . . 10 (𝑦 = {𝐴} → (𝐴𝑦𝐴 ∈ {𝐴}))
13 sseq1 3164 . . . . . . . . . 10 (𝑦 = {𝐴} → (𝑦 ⊆ (𝑓𝑥) ↔ {𝐴} ⊆ (𝑓𝑥)))
1412, 13anbi12d 465 . . . . . . . . 9 (𝑦 = {𝐴} → ((𝐴𝑦𝑦 ⊆ (𝑓𝑥)) ↔ (𝐴 ∈ {𝐴} ∧ {𝐴} ⊆ (𝑓𝑥))))
1514rspcev 2829 . . . . . . . 8 (({𝐴} ∈ 𝐽 ∧ (𝐴 ∈ {𝐴} ∧ {𝐴} ⊆ (𝑓𝑥))) → ∃𝑦𝐽 (𝐴𝑦𝑦 ⊆ (𝑓𝑥)))
161, 4, 11, 15syl12anc 1226 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ (𝑥𝐾 ∧ (𝑓𝐴) ∈ 𝑥)) → ∃𝑦𝐽 (𝐴𝑦𝑦 ⊆ (𝑓𝑥)))
1716expr 373 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) ∧ 𝑥𝐾) → ((𝑓𝐴) ∈ 𝑥 → ∃𝑦𝐽 (𝐴𝑦𝑦 ⊆ (𝑓𝑥))))
1817ralrimiva 2538 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ ({𝐴} ∈ 𝐽𝑓:𝑋𝑌)) → ∀𝑥𝐾 ((𝑓𝐴) ∈ 𝑥 → ∃𝑦𝐽 (𝐴𝑦𝑦 ⊆ (𝑓𝑥))))
1918expr 373 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓:𝑋𝑌 → ∀𝑥𝐾 ((𝑓𝐴) ∈ 𝑥 → ∃𝑦𝐽 (𝐴𝑦𝑦 ⊆ (𝑓𝑥)))))
2019pm4.71d 391 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓:𝑋𝑌 ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝐾 ((𝑓𝐴) ∈ 𝑥 → ∃𝑦𝐽 (𝐴𝑦𝑦 ⊆ (𝑓𝑥))))))
21 simpl2 991 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → 𝐾 ∈ (TopOn‘𝑌))
22 toponmax 12623 . . . . 5 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
2321, 22syl 14 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → 𝑌𝐾)
24 simpl1 990 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → 𝐽 ∈ (TopOn‘𝑋))
25 toponmax 12623 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
2624, 25syl 14 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → 𝑋𝐽)
2723, 26elmapd 6624 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓 ∈ (𝑌𝑚 𝑋) ↔ 𝑓:𝑋𝑌))
28 iscnp3 12803 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) → (𝑓 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝐾 ((𝑓𝐴) ∈ 𝑥 → ∃𝑦𝐽 (𝐴𝑦𝑦 ⊆ (𝑓𝑥))))))
2928adantr 274 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝑓:𝑋𝑌 ∧ ∀𝑥𝐾 ((𝑓𝐴) ∈ 𝑥 → ∃𝑦𝐽 (𝐴𝑦𝑦 ⊆ (𝑓𝑥))))))
3020, 27, 293bitr4rd 220 . 2 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ 𝑓 ∈ (𝑌𝑚 𝑋)))
3130eqrdv 2163 1 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ {𝐴} ∈ 𝐽) → ((𝐽 CnP 𝐾)‘𝐴) = (𝑌𝑚 𝑋))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 968   = wceq 1343  wcel 2136  wral 2443  wrex 2444  wss 3115  {csn 3575  ccnv 4602  cima 4606   Fn wfn 5182  wf 5183  cfv 5187  (class class class)co 5841  𝑚 cmap 6610  TopOnctopon 12608   CnP ccnp 12786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-sep 4099  ax-pow 4152  ax-pr 4186  ax-un 4410  ax-setind 4513
This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ne 2336  df-ral 2448  df-rex 2449  df-rab 2452  df-v 2727  df-sbc 2951  df-csb 3045  df-dif 3117  df-un 3119  df-in 3121  df-ss 3128  df-pw 3560  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-iun 3867  df-br 3982  df-opab 4043  df-mpt 4044  df-id 4270  df-xp 4609  df-rel 4610  df-cnv 4611  df-co 4612  df-dm 4613  df-rn 4614  df-res 4615  df-ima 4616  df-iota 5152  df-fun 5189  df-fn 5190  df-f 5191  df-fv 5195  df-ov 5844  df-oprab 5845  df-mpo 5846  df-1st 6105  df-2nd 6106  df-map 6612  df-top 12596  df-topon 12609  df-cnp 12789
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator