Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  kelac2 Unicode version

Theorem kelac2 26848
 Description: Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Hypotheses
Ref Expression
kelac2.s
kelac2.z
kelac2.k
Assertion
Ref Expression
kelac2
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem kelac2
StepHypRef Expression
1 kelac2.z . 2
2 kelac2.s . . 3
3 kelac2lem 26847 . . 3
4 cmptop 17394 . . 3
52, 3, 43syl 19 . 2
6 uncom 3448 . . . . . . 7
76difeq1i 3418 . . . . . 6
8 difun2 3664 . . . . . 6
97, 8eqtri 2421 . . . . 5
10 snex 4360 . . . . . . 7
11 uniprg 3986 . . . . . . 7
122, 10, 11sylancl 644 . . . . . 6
1312difeq1d 3421 . . . . 5
14 incom 3490 . . . . . . 7
15 pwuninel 6495 . . . . . . . . 9
1615a1i 11 . . . . . . . 8
17 disjsn 3825 . . . . . . . 8
1816, 17sylibr 204 . . . . . . 7
1914, 18syl5eq 2445 . . . . . 6
20 disj3 3629 . . . . . 6
2119, 20sylib 189 . . . . 5
229, 13, 213eqtr4a 2459 . . . 4
23 prex 4361 . . . . . 6
24 bastg 16968 . . . . . 6
2523, 24mp1i 12 . . . . 5
2610prid2 3870 . . . . . 6
2726a1i 11 . . . . 5
2825, 27sseldd 3306 . . . 4
2922, 28eqeltrd 2475 . . 3
30 prid1g 3867 . . . . 5
31 elssuni 3999 . . . . 5
322, 30, 313syl 19 . . . 4
33 unitg 16969 . . . . . . 7
3423, 33ax-mp 8 . . . . . 6
3534eqcomi 2405 . . . . 5
3635iscld2 17029 . . . 4
375, 32, 36syl2anc 643 . . 3
3829, 37mpbird 224 . 2
39 f1oi 5667 . . 3
4039a1i 11 . 2
41 elssuni 3999 . . . . 5
4226, 41mp1i 12 . . . 4
43 uniexg 4660 . . . . . 6
44 pwexg 4338 . . . . . 6
452, 43, 443syl 19 . . . . 5
46 snidg 3796 . . . . 5
4745, 46syl 16 . . . 4
4842, 47sseldd 3306 . . 3
4948, 34syl6eleqr 2492 . 2
50 kelac2.k . 2
511, 5, 38, 40, 49, 50kelac1 26846 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wceq 1649   wcel 1721   wne 2564  cvv 2913   cdif 3274   cun 3275   cin 3276   wss 3277  c0 3585  cpw 3756  csn 3771  cpr 3772  cuni 3971   cmpt 4221   cid 4448   cres 4834  wf1o 5407  cfv 5408  cixp 7013  ctg 13606  cpt 13607  ctop 16895  ccld 17017  ccmp 17385 This theorem is referenced by:  dfac21  26849 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-iin 4052  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-recs 6583  df-rdg 6618  df-1o 6674  df-2o 6675  df-oadd 6678  df-er 6855  df-map 6970  df-ixp 7014  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-fi 7365  df-topgen 13608  df-pt 13609  df-top 16900  df-bases 16902  df-cld 17020  df-cmp 17386
 Copyright terms: Public domain W3C validator