Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heiborlem1 Structured version   Unicode version

Theorem heiborlem1 32050
 Description: Lemma for heibor 32060. We work with a fixed open cover throughout. The set is the set of all subsets of that admit no finite subcover of . (We wish to prove that is empty.) If a set has no finite subcover, then any finite cover of must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014.)
Hypotheses
Ref Expression
heibor.1
heibor.3
heiborlem1.4
Assertion
Ref Expression
heiborlem1
Distinct variable groups:   ,   ,,,   ,,   ,,,   ,,,   ,,   ,
Allowed substitution hints:   (,)   ()   ()   (,)

Proof of Theorem heiborlem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 heiborlem1.4 . . . . . . . 8
2 sseq1 3428 . . . . . . . . . 10
32rexbidv 2878 . . . . . . . . 9
43notbid 295 . . . . . . . 8
5 heibor.3 . . . . . . . 8
61, 4, 5elab2 3163 . . . . . . 7
76con2bii 333 . . . . . 6
87ralbii 2796 . . . . 5
9 ralnex 2811 . . . . 5
108, 9bitr2i 253 . . . 4
11 unieq 4170 . . . . . . . . 9
1211sseq2d 3435 . . . . . . . 8
1312ac6sfi 7768 . . . . . . 7
1413ex 435 . . . . . 6
1514adantr 466 . . . . 5
16 sseq1 3428 . . . . . . . . . . . 12
1716rexbidv 2878 . . . . . . . . . . 11
1817notbid 295 . . . . . . . . . 10
1918, 5elab2g 3162 . . . . . . . . 9
2019ibi 244 . . . . . . . 8
21 frn 5695 . . . . . . . . . . . . . . 15
2221ad2antrl 732 . . . . . . . . . . . . . 14
23 inss1 3625 . . . . . . . . . . . . . 14
2422, 23syl6ss 3419 . . . . . . . . . . . . 13
25 sspwuni 4331 . . . . . . . . . . . . 13
2624, 25sylib 199 . . . . . . . . . . . 12
27 vex 3025 . . . . . . . . . . . . . . 15
2827rnex 6685 . . . . . . . . . . . . . 14
2928uniex 6545 . . . . . . . . . . . . 13
3029elpw 3930 . . . . . . . . . . . 12
3126, 30sylibr 215 . . . . . . . . . . 11
32 ffn 5689 . . . . . . . . . . . . . . 15
3332ad2antrl 732 . . . . . . . . . . . . . 14
34 dffn4 5759 . . . . . . . . . . . . . 14
3533, 34sylib 199 . . . . . . . . . . . . 13
36 fofi 7813 . . . . . . . . . . . . 13
3735, 36syldan 472 . . . . . . . . . . . 12
38 inss2 3626 . . . . . . . . . . . . 13
3922, 38syl6ss 3419 . . . . . . . . . . . 12
40 unifi 7816 . . . . . . . . . . . 12
4137, 39, 40syl2anc 665 . . . . . . . . . . 11
4231, 41elind 3593 . . . . . . . . . 10
4342adantlr 719 . . . . . . . . 9
44 simplr 760 . . . . . . . . . 10
45 fnfvelrn 5978 . . . . . . . . . . . . . . . . . 18
4632, 45sylan 473 . . . . . . . . . . . . . . . . 17
4746adantll 718 . . . . . . . . . . . . . . . 16
48 elssuni 4191 . . . . . . . . . . . . . . . 16
49 uniss 4183 . . . . . . . . . . . . . . . 16
5047, 48, 493syl 18 . . . . . . . . . . . . . . 15
51 sstr2 3414 . . . . . . . . . . . . . . 15
5250, 51syl5com 31 . . . . . . . . . . . . . 14
5352ralimdva 2773 . . . . . . . . . . . . 13
5453impr 623 . . . . . . . . . . . 12
55 iunss 4283 . . . . . . . . . . . 12
5654, 55sylibr 215 . . . . . . . . . . 11
5756adantlr 719 . . . . . . . . . 10
5844, 57sstrd 3417 . . . . . . . . 9
59 unieq 4170 . . . . . . . . . . 11
6059sseq2d 3435 . . . . . . . . . 10
6160rspcev 3125 . . . . . . . . 9
6243, 58, 61syl2anc 665 . . . . . . . 8
6320, 62nsyl3 122 . . . . . . 7
6463ex 435 . . . . . 6
6564exlimdv 1772 . . . . 5
6615, 65syld 45 . . . 4
6710, 66syl5bi 220 . . 3
6867con4d 108 . 2
69683impia 1202 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 370   w3a 982   wceq 1437  wex 1657   wcel 1872  cab 2414  wral 2714  wrex 2715  cvv 3022   cin 3378   wss 3379  cpw 3924  cuni 4162  ciun 4242   crn 4797   wfn 5539  wf 5540  wfo 5542  cfv 5544  cfn 7524  cmopn 18903 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-en 7525  df-dom 7526  df-fin 7528 This theorem is referenced by:  heiborlem3  32052  heiborlem10  32059
 Copyright terms: Public domain W3C validator