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

Theorem wunpw 10732
Description: A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wununi.1 (𝜑𝑈 ∈ WUni)
wununi.2 (𝜑𝐴𝑈)
Assertion
Ref Expression
wunpw (𝜑 → 𝒫 𝐴𝑈)

Proof of Theorem wunpw
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pweq 4618 . . 3 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
21eleq1d 2810 . 2 (𝑥 = 𝐴 → (𝒫 𝑥𝑈 ↔ 𝒫 𝐴𝑈))
3 wununi.1 . . 3 (𝜑𝑈 ∈ WUni)
4 iswun 10729 . . . . 5 (𝑈 ∈ WUni → (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑥𝑈 ( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈))))
54ibi 266 . . . 4 (𝑈 ∈ WUni → (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑥𝑈 ( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈)))
65simp3d 1141 . . 3 (𝑈 ∈ WUni → ∀𝑥𝑈 ( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈))
7 simp2 1134 . . . 4 (( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈) → 𝒫 𝑥𝑈)
87ralimi 3072 . . 3 (∀𝑥𝑈 ( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈) → ∀𝑥𝑈 𝒫 𝑥𝑈)
93, 6, 83syl 18 . 2 (𝜑 → ∀𝑥𝑈 𝒫 𝑥𝑈)
10 wununi.2 . 2 (𝜑𝐴𝑈)
112, 9, 10rspcdva 3607 1 (𝜑 → 𝒫 𝐴𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1533  wcel 2098  wne 2929  wral 3050  c0 4322  𝒫 cpw 4604  {cpr 4632   cuni 4909  Tr wtr 5266  WUnicwun 10725
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-v 3463  df-ss 3961  df-pw 4606  df-uni 4910  df-tr 5267  df-wun 10727
This theorem is referenced by:  wunss  10737  wunr1om  10744  wunxp  10749  wunpm  10750  intwun  10760  r1wunlim  10762  wuncval2  10772  wuncn  11195  wunfunc  17890  wunfuncOLD  17891  wunnat  17949  wunnatOLD  17950  catcoppccl  18109  catcoppcclOLD  18110  catcfuccl  18111  catcfucclOLD  18112  catcxpccl  18201  catcxpcclOLD  18202  ex-sategoelel  35162
  Copyright terms: Public domain W3C validator