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

Theorem ptcmp 24230
Description: Tychonoff's theorem: The product of compact spaces is compact. The proof uses the Axiom of Choice. (Contributed by Mario Carneiro, 26-Aug-2015.)
Assertion
Ref Expression
ptcmp ((𝐴𝑉𝐹:𝐴⟶Comp) → (∏t𝐹) ∈ Comp)

Proof of Theorem ptcmp
StepHypRef Expression
1 fvex 6898 . . . . 5 (∏t𝐹) ∈ V
21uniex 7745 . . . 4 (∏t𝐹) ∈ V
3 axac3 10458 . . . . 5 CHOICE
4 acufl 24089 . . . . 5 (CHOICE → UFL = V)
53, 4ax-mp 5 . . . 4 UFL = V
62, 5eleqtrri 2865 . . 3 (∏t𝐹) ∈ UFL
7 cardeqv 10463 . . . 4 dom card = V
82, 7eleqtrri 2865 . . 3 (∏t𝐹) ∈ dom card
96, 8elini 4155 . 2 (∏t𝐹) ∈ (UFL ∩ dom card)
10 eqid 2766 . . 3 (∏t𝐹) = (∏t𝐹)
11 eqid 2766 . . 3 (∏t𝐹) = (∏t𝐹)
1210, 11ptcmpg 24229 . 2 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ (∏t𝐹) ∈ (UFL ∩ dom card)) → (∏t𝐹) ∈ Comp)
139, 12mp3an3 1479 1 ((𝐴𝑉𝐹:𝐴⟶Comp) → (∏t𝐹) ∈ Comp)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wa 401   = wceq 1570  wcel 2146  Vcvv 3458  cin 3907   cuni 4875  dom cdm 5664  wf 6536  cfv 6540  cardccrd 9932  CHOICEwac 10110  tcpt 17501  Compccmp 23558  UFLcufl 24072
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5241  ax-sep 5260  ax-nul 5272  ax-pow 5339  ax-pr 5407  ax-un 7738  ax-ac2 10457
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-int 4916  df-iun 4961  df-iin 4962  df-br 5113  df-opab 5177  df-mpt 5196  df-tr 5222  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-rpss 7726  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-oadd 8459  df-omul 8460  df-er 8696  df-map 8828  df-ixp 8898  df-en 8946  df-dom 8947  df-fin 8949  df-fi 9373  df-wdom 9529  df-dju 9898  df-card 9936  df-acn 9939  df-ac 10111  df-topgen 17506  df-pt 17507  df-fbas 21534  df-fg 21535  df-top 23066  df-topon 23083  df-bases 23118  df-cld 23191  df-ntr 23192  df-cls 23193  df-nei 23270  df-cmp 23559  df-fil 24018  df-ufil 24073  df-ufl 24074  df-flim 24111  df-fcls 24113
This theorem is used by: (None)
  Copyright terms: Public domain W3C validator