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

Theorem kelac1 27152
 Description: Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Hypotheses
Ref Expression
kelac1.z
kelac1.j
kelac1.c
kelac1.b
kelac1.u
kelac1.k
Assertion
Ref Expression
kelac1
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()

Proof of Theorem kelac1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kelac1.c . . . . . . 7
2 eqid 2438 . . . . . . . 8
32cldss 17098 . . . . . . 7
41, 3syl 16 . . . . . 6
54ralrimiva 2791 . . . . 5
6 boxriin 7107 . . . . 5
75, 6syl 16 . . . 4
8 kelac1.k . . . . . . . . 9
9 cmptop 17463 . . . . . . . . 9
10 0ntop 16983 . . . . . . . . . . 11
11 fvprc 5725 . . . . . . . . . . . 12
1211eleq1d 2504 . . . . . . . . . . 11
1310, 12mtbiri 296 . . . . . . . . . 10
1413con4i 125 . . . . . . . . 9
158, 9, 143syl 19 . . . . . . . 8
16 kelac1.j . . . . . . . . 9
17 eqid 2438 . . . . . . . . 9
1816, 17fmptd 5896 . . . . . . . 8
19 dmfex 5629 . . . . . . . 8
2015, 18, 19syl2anc 644 . . . . . . 7
2116ralrimiva 2791 . . . . . . 7
22 eqid 2438 . . . . . . . 8
2322ptunimpt 17632 . . . . . . 7
2420, 21, 23syl2anc 644 . . . . . 6
2524ineq1d 3543 . . . . 5
26 eqid 2438 . . . . . 6
272topcld 17104 . . . . . . . . . 10
2816, 27syl 16 . . . . . . . . 9
29 ifcl 3777 . . . . . . . . 9
301, 28, 29syl2anc 644 . . . . . . . 8
3120, 16, 30ptcldmpt 17651 . . . . . . 7
3231adantr 453 . . . . . 6
33 simprr 735 . . . . . . . 8
34 kelac1.b . . . . . . . . . . . . . . 15
35 f1ofo 5684 . . . . . . . . . . . . . . 15
36 foima 5661 . . . . . . . . . . . . . . 15
3734, 35, 363syl 19 . . . . . . . . . . . . . 14
3837eqcomd 2443 . . . . . . . . . . . . 13
39 kelac1.z . . . . . . . . . . . . . 14
40 f1ofn 5678 . . . . . . . . . . . . . . . . 17
4134, 40syl 16 . . . . . . . . . . . . . . . 16
42 ssid 3369 . . . . . . . . . . . . . . . 16
43 fnimaeq0 5569 . . . . . . . . . . . . . . . 16
4441, 42, 43sylancl 645 . . . . . . . . . . . . . . 15
4544necon3bid 2638 . . . . . . . . . . . . . 14
4639, 45mpbird 225 . . . . . . . . . . . . 13
4738, 46eqnetrd 2621 . . . . . . . . . . . 12
48 n0 3639 . . . . . . . . . . . 12
4947, 48sylib 190 . . . . . . . . . . 11
50 rexv 2972 . . . . . . . . . . 11
5149, 50sylibr 205 . . . . . . . . . 10
5251ralrimiva 2791 . . . . . . . . 9
53 ssralv 3409 . . . . . . . . . 10
5453adantr 453 . . . . . . . . 9
5552, 54mpan9 457 . . . . . . . 8
56 eleq1 2498 . . . . . . . . 9
5756ac6sfi 7354 . . . . . . . 8
5833, 55, 57syl2anc 644 . . . . . . 7
5924eqcomd 2443 . . . . . . . . . . 11
6059ineq1d 3543 . . . . . . . . . 10
6160ad2antrr 708 . . . . . . . . 9
62 iftrue 3747 . . . . . . . . . . . . . . . . . . 19
6362ad2antrl 710 . . . . . . . . . . . . . . . . . 18
64 simpll 732 . . . . . . . . . . . . . . . . . . . . 21
65 simprl 734 . . . . . . . . . . . . . . . . . . . . . 22
6665sselda 3350 . . . . . . . . . . . . . . . . . . . . 21
6764, 66, 4syl2anc 644 . . . . . . . . . . . . . . . . . . . 20
6867sseld 3349 . . . . . . . . . . . . . . . . . . 19
6968impr 604 . . . . . . . . . . . . . . . . . 18
7063, 69eqeltrd 2512 . . . . . . . . . . . . . . . . 17
7170expr 600 . . . . . . . . . . . . . . . 16
7271ralimdva 2786 . . . . . . . . . . . . . . 15
7372imp 420 . . . . . . . . . . . . . 14
74 eldifn 3472 . . . . . . . . . . . . . . . . . . 19
75 iffalse 3748 . . . . . . . . . . . . . . . . . . 19
7674, 75syl 16 . . . . . . . . . . . . . . . . . 18
7776adantl 454 . . . . . . . . . . . . . . . . 17
78 eldifi 3471 . . . . . . . . . . . . . . . . . 18
79 kelac1.u . . . . . . . . . . . . . . . . . 18
8078, 79sylan2 462 . . . . . . . . . . . . . . . . 17
8177, 80eqeltrd 2512 . . . . . . . . . . . . . . . 16
8281ralrimiva 2791 . . . . . . . . . . . . . . 15
8382ad2antrr 708 . . . . . . . . . . . . . 14
84 ralun 3531 . . . . . . . . . . . . . 14
8573, 83, 84syl2anc 644 . . . . . . . . . . . . 13
86 undif 3710 . . . . . . . . . . . . . . . . 17
8786biimpi 188 . . . . . . . . . . . . . . . 16
8887ad2antrl 710 . . . . . . . . . . . . . . 15
8988raleqdv 2912 . . . . . . . . . . . . . 14
9089adantr 453 . . . . . . . . . . . . 13
9185, 90mpbid 203 . . . . . . . . . . . 12
9220ad2antrr 708 . . . . . . . . . . . . 13
93 mptelixpg 7102 . . . . . . . . . . . . 13
9492, 93syl 16 . . . . . . . . . . . 12
9591, 94mpbird 225 . . . . . . . . . . 11
96 eleq2 2499 . . . . . . . . . . . . . . . . . . . . . 22
97 eleq2 2499 . . . . . . . . . . . . . . . . . . . . . 22
98 simplrr 739 . . . . . . . . . . . . . . . . . . . . . 22
9969adantr 453 . . . . . . . . . . . . . . . . . . . . . 22
10096, 97, 98, 99ifbothda 3771 . . . . . . . . . . . . . . . . . . . . 21
10163, 100eqeltrd 2512 . . . . . . . . . . . . . . . . . . . 20
102101expr 600 . . . . . . . . . . . . . . . . . . 19
103102ralimdva 2786 . . . . . . . . . . . . . . . . . 18
104103imp 420 . . . . . . . . . . . . . . . . 17
105104adantr 453 . . . . . . . . . . . . . . . 16
10680adantlr 697 . . . . . . . . . . . . . . . . . . . 20
10776adantl 454 . . . . . . . . . . . . . . . . . . . 20
108 incom 3535 . . . . . . . . . . . . . . . . . . . . . . . . 25
109 disjdif 3702 . . . . . . . . . . . . . . . . . . . . . . . . 25
110108, 109eqtri 2458 . . . . . . . . . . . . . . . . . . . . . . . 24
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
112 simpr 449 . . . . . . . . . . . . . . . . . . . . . . 23
113 simplr 733 . . . . . . . . . . . . . . . . . . . . . . 23
114 disjne 3675 . . . . . . . . . . . . . . . . . . . . . . 23
115111, 112, 113, 114syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . 22
116115neneqd 2619 . . . . . . . . . . . . . . . . . . . . 21
117 iffalse 3748 . . . . . . . . . . . . . . . . . . . . 21
118116, 117syl 16 . . . . . . . . . . . . . . . . . . . 20
119106, 107, 1183eltr4d 2519 . . . . . . . . . . . . . . . . . . 19
120119ralrimiva 2791 . . . . . . . . . . . . . . . . . 18
121120adantlr 697 . . . . . . . . . . . . . . . . 17
122121adantlr 697 . . . . . . . . . . . . . . . 16
123 ralun 3531 . . . . . . . . . . . . . . . 16
124105, 122, 123syl2anc 644 . . . . . . . . . . . . . . 15
12588raleqdv 2912 . . . . . . . . . . . . . . . 16
126125ad2antrr 708 . . . . . . . . . . . . . . 15
127124, 126mpbid 203 . . . . . . . . . . . . . 14
12820ad3antrrr 712 . . . . . . . . . . . . . . 15
129 mptelixpg 7102 . . . . . . . . . . . . . . 15
130128, 129syl 16 . . . . . . . . . . . . . 14
131127, 130mpbird 225 . . . . . . . . . . . . 13
132131ralrimiva 2791 . . . . . . . . . . . 12
133 mptexg 5968 . . . . . . . . . . . . . . 15
13420, 133syl 16 . . . . . . . . . . . . . 14
135134ad2antrr 708 . . . . . . . . . . . . 13
136 eliin 4100 . . . . . . . . . . . . 13
137135, 136syl 16 . . . . . . . . . . . 12
138132, 137mpbird 225 . . . . . . . . . . 11
139 elin 3532 . . . . . . . . . . 11
14095, 138, 139sylanbrc 647 . . . . . . . . . 10
141 ne0i 3636 . . . . . . . . . 10
142140, 141syl 16 . . . . . . . . 9
14361, 142eqnetrd 2621 . . . . . . . 8
144143adantrl 698 . . . . . . 7
14558, 144exlimddv 1649 . . . . . 6
14626, 8, 32, 145cmpfiiin 26765 . . . . 5
14725, 146eqnetrd 2621 . . . 4
1487, 147eqnetrd 2621 . . 3
149 n0 3639 . . 3
150148, 149sylib 190 . 2
151 elixp2 7069 . . . . . 6
152151simp3bi 975 . . . . 5
153 f1ocnv 5690 . . . . . . . 8
154 f1of 5677 . . . . . . . 8
155 ffvelrn 5871 . . . . . . . . 9
156155ex 425 . . . . . . . 8
15734, 153, 154, 1564syl 20 . . . . . . 7
158157ralimdva 2786 . . . . . 6
159158imp 420 . . . . 5
160152, 159sylan2 462 . . . 4
161 mptelixpg 7102 . . . . . 6
16220, 161syl 16 . . . . 5
163162adantr 453 . . . 4
164160, 163mpbird 225 . . 3
165 ne0i 3636 . . 3
166164, 165syl 16 . 2
167150, 166exlimddv 1649 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360  wex 1551   wceq 1653   wcel 1726   wne 2601  wral 2707  wrex 2708  cvv 2958   cdif 3319   cun 3320   cin 3321   wss 3322  c0 3630  cif 3741  cuni 4017  ciin 4096   cmpt 4269  ccnv 4880  cima 4884   wfn 5452  wf 5453  wfo 5455  wf1o 5456  cfv 5457  cixp 7066  cfn 7112  cpt 13671  ctop 16963  ccld 17085  ccmp 17454 This theorem is referenced by:  kelac2  27154 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-recs 6636  df-rdg 6671  df-1o 6727  df-2o 6728  df-oadd 6731  df-er 6908  df-map 7023  df-ixp 7067  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-fi 7419  df-topgen 13672  df-pt 13673  df-top 16968  df-bases 16970  df-cld 17088  df-cmp 17455
 Copyright terms: Public domain W3C validator