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

Theorem fiinopn 11766
Description: The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.)
Assertion
Ref Expression
fiinopn (𝐽 ∈ Top → ((𝐴𝐽𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → 𝐴𝐽))

Proof of Theorem fiinopn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elpwg 3443 . . . . . . 7 (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐽𝐴𝐽))
2 sseq1 3050 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝑥𝐽𝐴𝐽))
3 neeq1 2269 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝑥 ≠ ∅ ↔ 𝐴 ≠ ∅))
4 eleq1 2151 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝑥 ∈ Fin ↔ 𝐴 ∈ Fin))
52, 3, 43anbi123d 1249 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ((𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) ↔ (𝐴𝐽𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)))
6 inteq 3699 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 𝑥 = 𝐴)
76eleq1d 2157 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → ( 𝑥𝐽 𝐴𝐽))
87imbi2d 229 . . . . . . . . . . . . 13 (𝑥 = 𝐴 → ((𝐽 ∈ Top → 𝑥𝐽) ↔ (𝐽 ∈ Top → 𝐴𝐽)))
95, 8imbi12d 233 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (((𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → (𝐽 ∈ Top → 𝑥𝐽)) ↔ ((𝐴𝐽𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → (𝐽 ∈ Top → 𝐴𝐽))))
10 sp 1447 . . . . . . . . . . . . . 14 (∀𝑥((𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐽) → ((𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐽))
1110adantl 272 . . . . . . . . . . . . 13 ((∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥((𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐽)) → ((𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐽))
12 istopfin 11762 . . . . . . . . . . . . 13 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥((𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → 𝑥𝐽)))
1311, 12syl11 31 . . . . . . . . . . . 12 ((𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → (𝐽 ∈ Top → 𝑥𝐽))
149, 13vtoclg 2682 . . . . . . . . . . 11 (𝐴 ∈ 𝒫 𝐽 → ((𝐴𝐽𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → (𝐽 ∈ Top → 𝐴𝐽)))
1514com12 30 . . . . . . . . . 10 ((𝐴𝐽𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → (𝐴 ∈ 𝒫 𝐽 → (𝐽 ∈ Top → 𝐴𝐽)))
16153exp 1143 . . . . . . . . 9 (𝐴𝐽 → (𝐴 ≠ ∅ → (𝐴 ∈ Fin → (𝐴 ∈ 𝒫 𝐽 → (𝐽 ∈ Top → 𝐴𝐽)))))
1716com3r 79 . . . . . . . 8 (𝐴 ∈ Fin → (𝐴𝐽 → (𝐴 ≠ ∅ → (𝐴 ∈ 𝒫 𝐽 → (𝐽 ∈ Top → 𝐴𝐽)))))
1817com4r 86 . . . . . . 7 (𝐴 ∈ 𝒫 𝐽 → (𝐴 ∈ Fin → (𝐴𝐽 → (𝐴 ≠ ∅ → (𝐽 ∈ Top → 𝐴𝐽)))))
191, 18syl6bir 163 . . . . . 6 (𝐴 ∈ Fin → (𝐴𝐽 → (𝐴 ∈ Fin → (𝐴𝐽 → (𝐴 ≠ ∅ → (𝐽 ∈ Top → 𝐴𝐽))))))
2019pm2.43a 51 . . . . 5 (𝐴 ∈ Fin → (𝐴𝐽 → (𝐴𝐽 → (𝐴 ≠ ∅ → (𝐽 ∈ Top → 𝐴𝐽)))))
2120com4l 84 . . . 4 (𝐴𝐽 → (𝐴𝐽 → (𝐴 ≠ ∅ → (𝐴 ∈ Fin → (𝐽 ∈ Top → 𝐴𝐽)))))
2221pm2.43i 49 . . 3 (𝐴𝐽 → (𝐴 ≠ ∅ → (𝐴 ∈ Fin → (𝐽 ∈ Top → 𝐴𝐽))))
23223imp 1138 . 2 ((𝐴𝐽𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → (𝐽 ∈ Top → 𝐴𝐽))
2423com12 30 1 (𝐽 ∈ Top → ((𝐴𝐽𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → 𝐴𝐽))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 925  wal 1288   = wceq 1290  wcel 1439  wne 2256  wss 3002  c0 3289  𝒫 cpw 3435   cuni 3661   cint 3696  Fincfn 6513  Topctop 11759
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-nul 3973  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-iinf 4418
This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-v 2624  df-sbc 2844  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-nul 3290  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-int 3697  df-br 3854  df-opab 3908  df-id 4131  df-suc 4209  df-iom 4421  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-rn 4465  df-res 4466  df-ima 4467  df-iota 4995  df-fun 5032  df-fn 5033  df-f 5034  df-f1 5035  df-fo 5036  df-f1o 5037  df-fv 5038  df-er 6308  df-en 6514  df-fin 6516  df-top 11760
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator