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

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

Proof of Theorem wununi
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unieq 4920 . . 3 (𝑥 = 𝐴 𝑥 = 𝐴)
21eleq1d 2819 . 2 (𝑥 = 𝐴 → ( 𝑥𝑈 𝐴𝑈))
3 wununi.1 . . 3 (𝜑𝑈 ∈ WUni)
4 iswun 10699 . . . . 5 (𝑈 ∈ WUni → (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑥𝑈 ( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈))))
54ibi 267 . . . 4 (𝑈 ∈ WUni → (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑥𝑈 ( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈)))
65simp3d 1145 . . 3 (𝑈 ∈ WUni → ∀𝑥𝑈 ( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈))
7 simp1 1137 . . . 4 (( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈) → 𝑥𝑈)
87ralimi 3084 . . 3 (∀𝑥𝑈 ( 𝑥𝑈 ∧ 𝒫 𝑥𝑈 ∧ ∀𝑦𝑈 {𝑥, 𝑦} ∈ 𝑈) → ∀𝑥𝑈 𝑥𝑈)
93, 6, 83syl 18 . 2 (𝜑 → ∀𝑥𝑈 𝑥𝑈)
10 wununi.2 . 2 (𝜑𝐴𝑈)
112, 9, 10rspcdva 3614 1 (𝜑 𝐴𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088   = wceq 1542  wcel 2107  wne 2941  wral 3062  c0 4323  𝒫 cpw 4603  {cpr 4631   cuni 4909  Tr wtr 5266  WUnicwun 10695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267  df-wun 10697
This theorem is referenced by:  wunun  10705  wunint  10710  wundm  10723  wunrn  10724  wunfv  10727  intwun  10730  wuncval2  10742  wunstr  17121  wunfunc  17849  wunfuncOLD  17850  wunnat  17907  wunnatOLD  17908  catcoppccl  18067  catcoppcclOLD  18068  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160
  Copyright terms: Public domain W3C validator