Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  harwdom Structured version   Unicode version

Theorem harwdom 8051
 Description: The Hartogs function is weakly dominated by . This follows from a more precise analysis of the bound used in hartogs 8005 to prove that har is a set. (Contributed by Mario Carneiro, 15-May-2015.)
Assertion
Ref Expression
harwdom har *

Proof of Theorem harwdom
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2422 . . . . . 6 OrdIso OrdIso
2 eqid 2422 . . . . . 6
31, 2hartogslem1 8003 . . . . 5 OrdIso OrdIso OrdIso
43simp2i 1015 . . . 4 OrdIso
53simp1i 1014 . . . . 5 OrdIso
6 sqxpexg 6547 . . . . . 6
7 pwexg 4544 . . . . . 6
86, 7syl 17 . . . . 5
9 ssexg 4506 . . . . 5 OrdIso OrdIso
105, 8, 9sylancr 667 . . . 4 OrdIso
11 funex 6085 . . . 4 OrdIso OrdIso OrdIso
124, 10, 11sylancr 667 . . 3 OrdIso
13 funfn 5566 . . . . . 6 OrdIso OrdIso OrdIso
144, 13mpbi 211 . . . . 5 OrdIso OrdIso
1514a1i 11 . . . 4 OrdIso OrdIso
163simp3i 1016 . . . . 5 OrdIso
17 harval 8023 . . . . 5 har
1816, 17eqtr4d 2459 . . . 4 OrdIso har
19 df-fo 5543 . . . 4 OrdIso OrdIso har OrdIso OrdIso OrdIso har
2015, 18, 19sylanbrc 668 . . 3 OrdIso OrdIso har
21 fowdom 8032 . . 3 OrdIso OrdIso OrdIso har har * OrdIso
2212, 20, 21syl2anc 665 . 2 har * OrdIso
23 ssdomg 7562 . . . 4 OrdIso OrdIso
248, 5, 23mpisyl 21 . . 3 OrdIso
25 domwdom 8035 . . 3 OrdIso OrdIso *
2624, 25syl 17 . 2 OrdIso *
27 wdomtr 8036 . 2 har * OrdIso OrdIso * har *
2822, 26, 27syl2anc 665 1 har *
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437   wcel 1872  wrex 2709  crab 2712  cvv 3016   cdif 3369   wss 3372  cpw 3917   class class class wbr 4359  copab 4417   cep 4698   cid 4699   wwe 4747   cxp 4787   cdm 4789   crn 4790   cres 4791  con0 5378   wfun 5531   wfn 5532  wfo 5535  cfv 5537   cdom 7515  OrdIsocoi 7970  harchar 8017   * cwdom 8018 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 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534 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 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-se 4749  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-isom 5546  df-riota 6204  df-wrecs 6976  df-recs 7038  df-er 7311  df-en 7518  df-dom 7519  df-sdom 7520  df-oi 7971  df-har 8019  df-wdom 8020 This theorem is referenced by:  gchhar  9048
 Copyright terms: Public domain W3C validator