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

Theorem kqcldsat 21517
Description: Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 21501). (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
Assertion
Ref Expression
kqcldsat ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝐹𝑈)) = 𝑈)
Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝑋,𝑦
Allowed substitution hints:   𝑈(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem kqcldsat
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 kqval.2 . . . . . . 7 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
21kqffn 21509 . . . . . 6 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
3 elpreima 6323 . . . . . 6 (𝐹 Fn 𝑋 → (𝑧 ∈ (𝐹 “ (𝐹𝑈)) ↔ (𝑧𝑋 ∧ (𝐹𝑧) ∈ (𝐹𝑈))))
42, 3syl 17 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → (𝑧 ∈ (𝐹 “ (𝐹𝑈)) ↔ (𝑧𝑋 ∧ (𝐹𝑧) ∈ (𝐹𝑈))))
54adantr 481 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑧 ∈ (𝐹 “ (𝐹𝑈)) ↔ (𝑧𝑋 ∧ (𝐹𝑧) ∈ (𝐹𝑈))))
6 noel 3911 . . . . . . . 8 ¬ (𝐹𝑧) ∈ ∅
7 elin 3788 . . . . . . . . 9 ((𝐹𝑧) ∈ ((𝐹𝑈) ∩ (𝐹 “ (𝑋𝑈))) ↔ ((𝐹𝑧) ∈ (𝐹𝑈) ∧ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))))
8 incom 3797 . . . . . . . . . . 11 ((𝐹𝑈) ∩ (𝐹 “ (𝑋𝑈))) = ((𝐹 “ (𝑋𝑈)) ∩ (𝐹𝑈))
9 eqid 2620 . . . . . . . . . . . . . . . . . . . 20 𝐽 = 𝐽
109cldss 20814 . . . . . . . . . . . . . . . . . . 19 (𝑈 ∈ (Clsd‘𝐽) → 𝑈 𝐽)
1110adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 𝐽)
12 fndm 5978 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn 𝑋 → dom 𝐹 = 𝑋)
132, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOn‘𝑋) → dom 𝐹 = 𝑋)
14 toponuni 20700 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
1513, 14eqtrd 2654 . . . . . . . . . . . . . . . . . . 19 (𝐽 ∈ (TopOn‘𝑋) → dom 𝐹 = 𝐽)
1615adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → dom 𝐹 = 𝐽)
1711, 16sseqtr4d 3634 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ⊆ dom 𝐹)
1813adantr 481 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → dom 𝐹 = 𝑋)
1917, 18sseqtrd 3633 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈𝑋)
2019adantr 481 . . . . . . . . . . . . . . 15 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → 𝑈𝑋)
21 dfss4 3850 . . . . . . . . . . . . . . 15 (𝑈𝑋 ↔ (𝑋 ∖ (𝑋𝑈)) = 𝑈)
2220, 21sylib 208 . . . . . . . . . . . . . 14 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → (𝑋 ∖ (𝑋𝑈)) = 𝑈)
2322imaeq2d 5454 . . . . . . . . . . . . 13 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → (𝐹 “ (𝑋 ∖ (𝑋𝑈))) = (𝐹𝑈))
2423ineq2d 3806 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → ((𝐹 “ (𝑋𝑈)) ∩ (𝐹 “ (𝑋 ∖ (𝑋𝑈)))) = ((𝐹 “ (𝑋𝑈)) ∩ (𝐹𝑈)))
25 simpll 789 . . . . . . . . . . . . 13 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → 𝐽 ∈ (TopOn‘𝑋))
2614adantr 481 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑋 = 𝐽)
2726difeq1d 3719 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑋𝑈) = ( 𝐽𝑈))
289cldopn 20816 . . . . . . . . . . . . . . . 16 (𝑈 ∈ (Clsd‘𝐽) → ( 𝐽𝑈) ∈ 𝐽)
2928adantl 482 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → ( 𝐽𝑈) ∈ 𝐽)
3027, 29eqeltrd 2699 . . . . . . . . . . . . . 14 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑋𝑈) ∈ 𝐽)
3130adantr 481 . . . . . . . . . . . . 13 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → (𝑋𝑈) ∈ 𝐽)
321kqdisj 21516 . . . . . . . . . . . . 13 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋𝑈) ∈ 𝐽) → ((𝐹 “ (𝑋𝑈)) ∩ (𝐹 “ (𝑋 ∖ (𝑋𝑈)))) = ∅)
3325, 31, 32syl2anc 692 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → ((𝐹 “ (𝑋𝑈)) ∩ (𝐹 “ (𝑋 ∖ (𝑋𝑈)))) = ∅)
3424, 33eqtr3d 2656 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → ((𝐹 “ (𝑋𝑈)) ∩ (𝐹𝑈)) = ∅)
358, 34syl5eq 2666 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → ((𝐹𝑈) ∩ (𝐹 “ (𝑋𝑈))) = ∅)
3635eleq2d 2685 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ ((𝐹𝑈) ∩ (𝐹 “ (𝑋𝑈))) ↔ (𝐹𝑧) ∈ ∅))
377, 36syl5bbr 274 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → (((𝐹𝑧) ∈ (𝐹𝑈) ∧ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))) ↔ (𝐹𝑧) ∈ ∅))
386, 37mtbiri 317 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → ¬ ((𝐹𝑧) ∈ (𝐹𝑈) ∧ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))))
39 imnan 438 . . . . . . 7 (((𝐹𝑧) ∈ (𝐹𝑈) → ¬ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))) ↔ ¬ ((𝐹𝑧) ∈ (𝐹𝑈) ∧ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))))
4038, 39sylibr 224 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ (𝐹𝑈) → ¬ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))))
41 eldif 3577 . . . . . . . . . 10 (𝑧 ∈ (𝑋𝑈) ↔ (𝑧𝑋 ∧ ¬ 𝑧𝑈))
4241baibr 944 . . . . . . . . 9 (𝑧𝑋 → (¬ 𝑧𝑈𝑧 ∈ (𝑋𝑈)))
4342adantl 482 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → (¬ 𝑧𝑈𝑧 ∈ (𝑋𝑈)))
44 simpr 477 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → 𝑧𝑋)
451kqfvima 21514 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋𝑈) ∈ 𝐽𝑧𝑋) → (𝑧 ∈ (𝑋𝑈) ↔ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))))
4625, 31, 44, 45syl3anc 1324 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → (𝑧 ∈ (𝑋𝑈) ↔ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))))
4743, 46bitrd 268 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → (¬ 𝑧𝑈 ↔ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈))))
4847con1bid 345 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → (¬ (𝐹𝑧) ∈ (𝐹 “ (𝑋𝑈)) ↔ 𝑧𝑈))
4940, 48sylibd 229 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) ∧ 𝑧𝑋) → ((𝐹𝑧) ∈ (𝐹𝑈) → 𝑧𝑈))
5049expimpd 628 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → ((𝑧𝑋 ∧ (𝐹𝑧) ∈ (𝐹𝑈)) → 𝑧𝑈))
515, 50sylbid 230 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑧 ∈ (𝐹 “ (𝐹𝑈)) → 𝑧𝑈))
5251ssrdv 3601 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝐹𝑈)) ⊆ 𝑈)
53 sseqin2 3809 . . . 4 (𝑈 ⊆ dom 𝐹 ↔ (dom 𝐹𝑈) = 𝑈)
5417, 53sylib 208 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (dom 𝐹𝑈) = 𝑈)
55 dminss 5535 . . 3 (dom 𝐹𝑈) ⊆ (𝐹 “ (𝐹𝑈))
5654, 55syl6eqssr 3648 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ⊆ (𝐹 “ (𝐹𝑈)))
5752, 56eqssd 3612 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝐹 “ (𝐹𝑈)) = 𝑈)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  {crab 2913  cdif 3564  cin 3566  wss 3567  c0 3907   cuni 4427  cmpt 4720  ccnv 5103  dom cdm 5104  cima 5107   Fn wfn 5871  cfv 5876  TopOnctopon 20696  Clsdccld 20801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884  df-top 20680  df-topon 20697  df-cld 20804
This theorem is referenced by:  kqcld  21519
  Copyright terms: Public domain W3C validator