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

Theorem hauspwdom 22025
Description: Simplify the cardinal 𝐴↑ℕ of hausmapdom 22024 to 𝒫 𝐵 = 2↑𝐵 when 𝐵 is an infinite cardinal greater than 𝐴. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 30-Apr-2015.)
Hypothesis
Ref Expression
hauspwdom.1 𝑋 = 𝐽
Assertion
Ref Expression
hauspwdom (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵)

Proof of Theorem hauspwdom
StepHypRef Expression
1 hauspwdom.1 . . . 4 𝑋 = 𝐽
21hausmapdom 22024 . . 3 ((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) → ((cls‘𝐽)‘𝐴) ≼ (𝐴m ℕ))
32adantr 481 . 2 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ (𝐴m ℕ))
4 simprr 769 . . . 4 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ℕ ≼ 𝐵)
5 1nn 11641 . . . . 5 1 ∈ ℕ
6 noel 4299 . . . . . . 7 ¬ 1 ∈ ∅
7 eleq2 2905 . . . . . . 7 (ℕ = ∅ → (1 ∈ ℕ ↔ 1 ∈ ∅))
86, 7mtbiri 328 . . . . . 6 (ℕ = ∅ → ¬ 1 ∈ ℕ)
98adantr 481 . . . . 5 ((ℕ = ∅ ∧ 𝐴 = ∅) → ¬ 1 ∈ ℕ)
105, 9mt2 201 . . . 4 ¬ (ℕ = ∅ ∧ 𝐴 = ∅)
11 mapdom2 8680 . . . 4 ((ℕ ≼ 𝐵 ∧ ¬ (ℕ = ∅ ∧ 𝐴 = ∅)) → (𝐴m ℕ) ≼ (𝐴m 𝐵))
124, 10, 11sylancl 586 . . 3 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴m ℕ) ≼ (𝐴m 𝐵))
13 sdomdom 8529 . . . . . . 7 (𝐴 ≺ 2o𝐴 ≼ 2o)
1413adantl 482 . . . . . 6 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2o) → 𝐴 ≼ 2o)
15 mapdom1 8674 . . . . . 6 (𝐴 ≼ 2o → (𝐴m 𝐵) ≼ (2om 𝐵))
1614, 15syl 17 . . . . 5 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2o) → (𝐴m 𝐵) ≼ (2om 𝐵))
17 reldom 8507 . . . . . . . . 9 Rel ≼
1817brrelex2i 5607 . . . . . . . 8 (ℕ ≼ 𝐵𝐵 ∈ V)
1918ad2antll 725 . . . . . . 7 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐵 ∈ V)
20 pw2eng 8615 . . . . . . 7 (𝐵 ∈ V → 𝒫 𝐵 ≈ (2om 𝐵))
21 ensym 8550 . . . . . . 7 (𝒫 𝐵 ≈ (2om 𝐵) → (2om 𝐵) ≈ 𝒫 𝐵)
2219, 20, 213syl 18 . . . . . 6 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (2om 𝐵) ≈ 𝒫 𝐵)
2322adantr 481 . . . . 5 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2o) → (2om 𝐵) ≈ 𝒫 𝐵)
24 domentr 8560 . . . . 5 (((𝐴m 𝐵) ≼ (2om 𝐵) ∧ (2om 𝐵) ≈ 𝒫 𝐵) → (𝐴m 𝐵) ≼ 𝒫 𝐵)
2516, 23, 24syl2anc 584 . . . 4 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2o) → (𝐴m 𝐵) ≼ 𝒫 𝐵)
26 onfin2 8702 . . . . . . . . 9 ω = (On ∩ Fin)
27 inss2 4209 . . . . . . . . 9 (On ∩ Fin) ⊆ Fin
2826, 27eqsstri 4004 . . . . . . . 8 ω ⊆ Fin
29 2onn 8259 . . . . . . . 8 2o ∈ ω
3028, 29sselii 3967 . . . . . . 7 2o ∈ Fin
31 simprl 767 . . . . . . . 8 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐴 ≼ 𝒫 𝐵)
3217brrelex1i 5606 . . . . . . . 8 (𝐴 ≼ 𝒫 𝐵𝐴 ∈ V)
3331, 32syl 17 . . . . . . 7 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐴 ∈ V)
34 fidomtri 9414 . . . . . . 7 ((2o ∈ Fin ∧ 𝐴 ∈ V) → (2o𝐴 ↔ ¬ 𝐴 ≺ 2o))
3530, 33, 34sylancr 587 . . . . . 6 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (2o𝐴 ↔ ¬ 𝐴 ≺ 2o))
3635biimpar 478 . . . . 5 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ ¬ 𝐴 ≺ 2o) → 2o𝐴)
37 numth3 9884 . . . . . . . . 9 (𝐵 ∈ V → 𝐵 ∈ dom card)
3819, 37syl 17 . . . . . . . 8 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐵 ∈ dom card)
3938adantr 481 . . . . . . 7 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o𝐴) → 𝐵 ∈ dom card)
40 nnenom 13341 . . . . . . . . . 10 ℕ ≈ ω
4140ensymi 8551 . . . . . . . . 9 ω ≈ ℕ
42 endomtr 8559 . . . . . . . . 9 ((ω ≈ ℕ ∧ ℕ ≼ 𝐵) → ω ≼ 𝐵)
4341, 4, 42sylancr 587 . . . . . . . 8 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ω ≼ 𝐵)
4443adantr 481 . . . . . . 7 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o𝐴) → ω ≼ 𝐵)
45 simpr 485 . . . . . . 7 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o𝐴) → 2o𝐴)
4631adantr 481 . . . . . . 7 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o𝐴) → 𝐴 ≼ 𝒫 𝐵)
47 mappwen 9530 . . . . . . 7 (((𝐵 ∈ dom card ∧ ω ≼ 𝐵) ∧ (2o𝐴𝐴 ≼ 𝒫 𝐵)) → (𝐴m 𝐵) ≈ 𝒫 𝐵)
4839, 44, 45, 46, 47syl22anc 836 . . . . . 6 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o𝐴) → (𝐴m 𝐵) ≈ 𝒫 𝐵)
49 endom 8528 . . . . . 6 ((𝐴m 𝐵) ≈ 𝒫 𝐵 → (𝐴m 𝐵) ≼ 𝒫 𝐵)
5048, 49syl 17 . . . . 5 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o𝐴) → (𝐴m 𝐵) ≼ 𝒫 𝐵)
5136, 50syldan 591 . . . 4 ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ ¬ 𝐴 ≺ 2o) → (𝐴m 𝐵) ≼ 𝒫 𝐵)
5225, 51pm2.61dan 809 . . 3 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴m 𝐵) ≼ 𝒫 𝐵)
53 domtr 8554 . . 3 (((𝐴m ℕ) ≼ (𝐴m 𝐵) ∧ (𝐴m 𝐵) ≼ 𝒫 𝐵) → (𝐴m ℕ) ≼ 𝒫 𝐵)
5412, 52, 53syl2anc 584 . 2 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴m ℕ) ≼ 𝒫 𝐵)
55 domtr 8554 . 2 ((((cls‘𝐽)‘𝐴) ≼ (𝐴m ℕ) ∧ (𝐴m ℕ) ≼ 𝒫 𝐵) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵)
563, 54, 55syl2anc 584 1 (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2106  Vcvv 3499  cin 3938  wss 3939  c0 4294  𝒫 cpw 4541   cuni 4836   class class class wbr 5062  dom cdm 5553  Oncon0 6188  cfv 6351  (class class class)co 7151  ωcom 7571  2oc2o 8090  m cmap 8399  cen 8498  cdom 8499  csdm 8500  Fincfn 8501  cardccrd 9356  1c1 10530  cn 11630  clsccl 21542  Hauscha 21832  1stωc1stc 21961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-inf2 9096  ax-cc 9849  ax-ac2 9877  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-map 8401  df-pm 8402  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-oi 8966  df-card 9360  df-acn 9363  df-ac 9534  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-n0 11890  df-z 11974  df-uz 12236  df-fz 12886  df-top 21418  df-topon 21435  df-cld 21543  df-ntr 21544  df-cls 21545  df-lm 21753  df-haus 21839  df-1stc 21963
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator