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

Theorem ptcmpg 22082
Description: Tychonoff's theorem: The product of compact spaces is compact. The choice principles needed are encoded in the last hypothesis: the base set of the product must be well-orderable and satisfy the ultrafilter lemma. Both these assumptions are satisfied if 𝒫 𝒫 𝑋 is well-orderable, so if we assume the Axiom of Choice we can eliminate them (see ptcmp 22083). (Contributed by Mario Carneiro, 27-Aug-2015.)
Hypotheses
Ref Expression
ptcmpg.1 𝐽 = (∏t𝐹)
ptcmpg.2 𝑋 = 𝐽
Assertion
Ref Expression
ptcmpg ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐽 ∈ Comp)

Proof of Theorem ptcmpg
Dummy variables 𝑎 𝑏 𝑘 𝑚 𝑛 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcmpg.1 . 2 𝐽 = (∏t𝐹)
2 nfcv 2913 . . . 4 𝑘(𝐹𝑎)
3 nfcv 2913 . . . 4 𝑎(𝐹𝑘)
4 nfcv 2913 . . . 4 𝑘((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑎)) “ 𝑏)
5 nfcv 2913 . . . 4 𝑢((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑎)) “ 𝑏)
6 nfcv 2913 . . . 4 𝑎((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)) “ 𝑢)
7 nfcv 2913 . . . 4 𝑏((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)) “ 𝑢)
8 fveq2 6333 . . . 4 (𝑎 = 𝑘 → (𝐹𝑎) = (𝐹𝑘))
9 fveq2 6333 . . . . . . . 8 (𝑎 = 𝑘 → (𝑤𝑎) = (𝑤𝑘))
109mpteq2dv 4880 . . . . . . 7 (𝑎 = 𝑘 → (𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑎)) = (𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)))
1110cnveqd 5437 . . . . . 6 (𝑎 = 𝑘(𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑎)) = (𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)))
1211imaeq1d 5607 . . . . 5 (𝑎 = 𝑘 → ((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑎)) “ 𝑏) = ((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)) “ 𝑏))
13 imaeq2 5604 . . . . 5 (𝑏 = 𝑢 → ((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)) “ 𝑏) = ((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)) “ 𝑢))
1412, 13sylan9eq 2825 . . . 4 ((𝑎 = 𝑘𝑏 = 𝑢) → ((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑎)) “ 𝑏) = ((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)) “ 𝑢))
152, 3, 4, 5, 6, 7, 8, 14cbvmpt2x 6881 . . 3 (𝑎𝐴, 𝑏 ∈ (𝐹𝑎) ↦ ((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑎)) “ 𝑏)) = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤X𝑛𝐴 (𝐹𝑛) ↦ (𝑤𝑘)) “ 𝑢))
16 fveq2 6333 . . . . 5 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
1716unieqd 4585 . . . 4 (𝑛 = 𝑚 (𝐹𝑛) = (𝐹𝑚))
1817cbvixpv 8081 . . 3 X𝑛𝐴 (𝐹𝑛) = X𝑚𝐴 (𝐹𝑚)
19 simp1 1130 . . 3 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐴𝑉)
20 simp2 1131 . . 3 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐹:𝐴⟶Comp)
21 cmptop 21420 . . . . . . . 8 (𝑘 ∈ Comp → 𝑘 ∈ Top)
2221ssriv 3757 . . . . . . 7 Comp ⊆ Top
23 fss 6197 . . . . . . 7 ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) → 𝐹:𝐴⟶Top)
2420, 22, 23sylancl 568 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐹:𝐴⟶Top)
251ptuni 21619 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) = 𝐽)
2619, 24, 25syl2anc 567 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → X𝑛𝐴 (𝐹𝑛) = 𝐽)
27 ptcmpg.2 . . . . 5 𝑋 = 𝐽
2826, 27syl6eqr 2823 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → X𝑛𝐴 (𝐹𝑛) = 𝑋)
29 simp3 1132 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝑋 ∈ (UFL ∩ dom card))
3028, 29eqeltrd 2850 . . 3 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → X𝑛𝐴 (𝐹𝑛) ∈ (UFL ∩ dom card))
3115, 18, 19, 20, 30ptcmplem5 22081 . 2 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → (∏t𝐹) ∈ Comp)
321, 31syl5eqel 2854 1 ((𝐴𝑉𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐽 ∈ Comp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071   = wceq 1631  wcel 2145  cin 3723  wss 3724   cuni 4575  cmpt 4864  ccnv 5249  dom cdm 5250  cima 5253  wf 6028  cfv 6032  cmpt2 6796  Xcixp 8063  cardccrd 8962  tcpt 16308  Topctop 20919  Compccmp 21411  UFLcufl 21925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-oadd 7718  df-omul 7719  df-er 7897  df-map 8012  df-ixp 8064  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-fi 8474  df-wdom 8621  df-card 8966  df-acn 8969  df-topgen 16313  df-pt 16314  df-fbas 19959  df-fg 19960  df-top 20920  df-topon 20937  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-cmp 21412  df-fil 21871  df-ufil 21926  df-ufl 21927  df-flim 21964  df-fcls 21966
This theorem is referenced by:  ptcmp  22083  dfac21  38163
  Copyright terms: Public domain W3C validator