Theorem wununi 10463

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.

Step	Hyp	Ref	Expression
1		unieq 4856	. . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴)
2	1	eleq1d 2825	. 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ 𝑈 ↔ ∪ 𝐴 ∈ 𝑈))
3		wununi.1	. . 3 ⊢ (𝜑 → 𝑈 ∈ WUni)
4		iswun 10461	. . . . 5 ⊢ (𝑈 ∈ WUni → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))))
5	4	ibi 266	. . . 4 ⊢ (𝑈 ∈ WUni → (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈)))
6	5	simp3d 1143	. . 3 ⊢ (𝑈 ∈ WUni → ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))
7		simp1 1135	. . . 4 ⊢ ((∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈) → ∪ 𝑥 ∈ 𝑈)
8	7	ralimi 3089	. . 3 ⊢ (∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈) → ∀𝑥 ∈ 𝑈 ∪ 𝑥 ∈ 𝑈)
9	3, 6, 8	3syl 18	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 ∪ 𝑥 ∈ 𝑈)
10		wununi.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
11	2, 9, 10	rspcdva 3563	1 ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1542   ∈ wcel 2110   ≠ wne 2945  ∀wral 3066  ∅c0 4262  𝒫 cpw 4539  {cpr 4569  ∪ cuni 4845  Tr wtr 5196  WUnicwun 10457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ne 2946  df-ral 3071  df-v 3433  df-in 3899  df-ss 3909  df-uni 4846  df-tr 5197  df-wun 10459

This theorem is referenced by:  wunun  10467  wunint  10472  wundm  10485  wunrn  10486  wunfv  10489  intwun  10492  wuncval2  10504  wunstr  16887  wunfunc  17612  wunfuncOLD  17613  wunnat  17670  wunnatOLD  17671  catcoppccl  17830  catcoppcclOLD  17831  catcfuccl  17832  catcfucclOLD  17833  catcxpccl  17922  catcxpcclOLD  17923