Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cmpfiiin Structured version   Visualization version   GIF version

Theorem cmpfiiin 41206
Description: In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Hypotheses
Ref Expression
cmpfiiin.x 𝑋 = 𝐽
cmpfiiin.j (𝜑𝐽 ∈ Comp)
cmpfiiin.s ((𝜑𝑘𝐼) → 𝑆 ∈ (Clsd‘𝐽))
cmpfiiin.z ((𝜑 ∧ (𝑙𝐼𝑙 ∈ Fin)) → (𝑋 𝑘𝑙 𝑆) ≠ ∅)
Assertion
Ref Expression
cmpfiiin (𝜑 → (𝑋 𝑘𝐼 𝑆) ≠ ∅)
Distinct variable groups:   𝜑,𝑘,𝑙   𝑘,𝐼,𝑙   𝑘,𝐽,𝑙   𝑆,𝑙   𝑘,𝑋,𝑙
Allowed substitution hint:   𝑆(𝑘)

Proof of Theorem cmpfiiin
StepHypRef Expression
1 cmpfiiin.j . . . . 5 (𝜑𝐽 ∈ Comp)
2 cmptop 22828 . . . . 5 (𝐽 ∈ Comp → 𝐽 ∈ Top)
31, 2syl 17 . . . 4 (𝜑𝐽 ∈ Top)
4 cmpfiiin.x . . . . 5 𝑋 = 𝐽
54topcld 22468 . . . 4 (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
63, 5syl 17 . . 3 (𝜑𝑋 ∈ (Clsd‘𝐽))
7 cmpfiiin.s . . . . 5 ((𝜑𝑘𝐼) → 𝑆 ∈ (Clsd‘𝐽))
84cldss 22462 . . . . 5 (𝑆 ∈ (Clsd‘𝐽) → 𝑆𝑋)
97, 8syl 17 . . . 4 ((𝜑𝑘𝐼) → 𝑆𝑋)
109ralrimiva 3145 . . 3 (𝜑 → ∀𝑘𝐼 𝑆𝑋)
11 riinint 5959 . . 3 ((𝑋 ∈ (Clsd‘𝐽) ∧ ∀𝑘𝐼 𝑆𝑋) → (𝑋 𝑘𝐼 𝑆) = ({𝑋} ∪ ran (𝑘𝐼𝑆)))
126, 10, 11syl2anc 584 . 2 (𝜑 → (𝑋 𝑘𝐼 𝑆) = ({𝑋} ∪ ran (𝑘𝐼𝑆)))
136snssd 4805 . . . 4 (𝜑 → {𝑋} ⊆ (Clsd‘𝐽))
147fmpttd 7099 . . . . 5 (𝜑 → (𝑘𝐼𝑆):𝐼⟶(Clsd‘𝐽))
1514frnd 6712 . . . 4 (𝜑 → ran (𝑘𝐼𝑆) ⊆ (Clsd‘𝐽))
1613, 15unssd 4182 . . 3 (𝜑 → ({𝑋} ∪ ran (𝑘𝐼𝑆)) ⊆ (Clsd‘𝐽))
17 elin 3960 . . . . . . 7 (𝑙 ∈ (𝒫 𝐼 ∩ Fin) ↔ (𝑙 ∈ 𝒫 𝐼𝑙 ∈ Fin))
18 elpwi 4603 . . . . . . . 8 (𝑙 ∈ 𝒫 𝐼𝑙𝐼)
1918anim1i 615 . . . . . . 7 ((𝑙 ∈ 𝒫 𝐼𝑙 ∈ Fin) → (𝑙𝐼𝑙 ∈ Fin))
2017, 19sylbi 216 . . . . . 6 (𝑙 ∈ (𝒫 𝐼 ∩ Fin) → (𝑙𝐼𝑙 ∈ Fin))
21 cmpfiiin.z . . . . . . 7 ((𝜑 ∧ (𝑙𝐼𝑙 ∈ Fin)) → (𝑋 𝑘𝑙 𝑆) ≠ ∅)
22 nesym 2996 . . . . . . 7 ((𝑋 𝑘𝑙 𝑆) ≠ ∅ ↔ ¬ ∅ = (𝑋 𝑘𝑙 𝑆))
2321, 22sylib 217 . . . . . 6 ((𝜑 ∧ (𝑙𝐼𝑙 ∈ Fin)) → ¬ ∅ = (𝑋 𝑘𝑙 𝑆))
2420, 23sylan2 593 . . . . 5 ((𝜑𝑙 ∈ (𝒫 𝐼 ∩ Fin)) → ¬ ∅ = (𝑋 𝑘𝑙 𝑆))
2524nrexdv 3148 . . . 4 (𝜑 → ¬ ∃𝑙 ∈ (𝒫 𝐼 ∩ Fin)∅ = (𝑋 𝑘𝑙 𝑆))
26 elrfirn2 41205 . . . . 5 ((𝑋 ∈ (Clsd‘𝐽) ∧ ∀𝑘𝐼 𝑆𝑋) → (∅ ∈ (fi‘({𝑋} ∪ ran (𝑘𝐼𝑆))) ↔ ∃𝑙 ∈ (𝒫 𝐼 ∩ Fin)∅ = (𝑋 𝑘𝑙 𝑆)))
276, 10, 26syl2anc 584 . . . 4 (𝜑 → (∅ ∈ (fi‘({𝑋} ∪ ran (𝑘𝐼𝑆))) ↔ ∃𝑙 ∈ (𝒫 𝐼 ∩ Fin)∅ = (𝑋 𝑘𝑙 𝑆)))
2825, 27mtbird 324 . . 3 (𝜑 → ¬ ∅ ∈ (fi‘({𝑋} ∪ ran (𝑘𝐼𝑆))))
29 cmpfii 22842 . . 3 ((𝐽 ∈ Comp ∧ ({𝑋} ∪ ran (𝑘𝐼𝑆)) ⊆ (Clsd‘𝐽) ∧ ¬ ∅ ∈ (fi‘({𝑋} ∪ ran (𝑘𝐼𝑆)))) → ({𝑋} ∪ ran (𝑘𝐼𝑆)) ≠ ∅)
301, 16, 28, 29syl3anc 1371 . 2 (𝜑 ({𝑋} ∪ ran (𝑘𝐼𝑆)) ≠ ∅)
3112, 30eqnetrd 3007 1 (𝜑 → (𝑋 𝑘𝐼 𝑆) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2939  wral 3060  wrex 3069  cun 3942  cin 3943  wss 3944  c0 4318  𝒫 cpw 4596  {csn 4622   cuni 4901   cint 4943   ciin 4991  cmpt 5224  ran crn 5670  cfv 6532  Fincfn 8922  ficfi 9387  Topctop 22324  Clsdccld 22449  Compccmp 22819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-om 7839  df-1o 8448  df-en 8923  df-fin 8926  df-fi 9388  df-top 22325  df-cld 22452  df-cmp 22820
This theorem is referenced by:  kelac1  41576
  Copyright terms: Public domain W3C validator