Theorem iswun 10115

Description: Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
iswun	⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))))

Distinct variable group:   𝑥,𝑦,𝑈

Allowed substitution hints:   𝑉(𝑥,𝑦)

Proof of Theorem iswun

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		treq 5142	. . 3 ⊢ (𝑧 = 𝑤 → (Tr 𝑧 ↔ Tr 𝑤))
2		neeq1 3049	. . 3 ⊢ (𝑧 = 𝑤 → (𝑧 ≠ ∅ ↔ 𝑤 ≠ ∅))
3		eleq2 2878	. . . . 5 ⊢ (𝑧 = 𝑤 → (∪ 𝑥 ∈ 𝑧 ↔ ∪ 𝑥 ∈ 𝑤))
4		eleq2 2878	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝒫 𝑥 ∈ 𝑧 ↔ 𝒫 𝑥 ∈ 𝑤))
5		eleq2 2878	. . . . . 6 ⊢ (𝑧 = 𝑤 → ({𝑥, 𝑦} ∈ 𝑧 ↔ {𝑥, 𝑦} ∈ 𝑤))
6	5	raleqbi1dv 3356	. . . . 5 ⊢ (𝑧 = 𝑤 → (∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧 ↔ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤))
7	3, 4, 6	3anbi123d 1433	. . . 4 ⊢ (𝑧 = 𝑤 → ((∪ 𝑥 ∈ 𝑧 ∧ 𝒫 𝑥 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧) ↔ (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤)))
8	7	raleqbi1dv 3356	. . 3 ⊢ (𝑧 = 𝑤 → (∀𝑥 ∈ 𝑧 (∪ 𝑥 ∈ 𝑧 ∧ 𝒫 𝑥 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧) ↔ ∀𝑥 ∈ 𝑤 (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤)))
9	1, 2, 8	3anbi123d 1433	. 2 ⊢ (𝑧 = 𝑤 → ((Tr 𝑧 ∧ 𝑧 ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 (∪ 𝑥 ∈ 𝑧 ∧ 𝒫 𝑥 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧)) ↔ (Tr 𝑤 ∧ 𝑤 ≠ ∅ ∧ ∀𝑥 ∈ 𝑤 (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤))))
10		treq 5142	. . 3 ⊢ (𝑤 = 𝑈 → (Tr 𝑤 ↔ Tr 𝑈))
11		neeq1 3049	. . 3 ⊢ (𝑤 = 𝑈 → (𝑤 ≠ ∅ ↔ 𝑈 ≠ ∅))
12		eleq2 2878	. . . . 5 ⊢ (𝑤 = 𝑈 → (∪ 𝑥 ∈ 𝑤 ↔ ∪ 𝑥 ∈ 𝑈))
13		eleq2 2878	. . . . 5 ⊢ (𝑤 = 𝑈 → (𝒫 𝑥 ∈ 𝑤 ↔ 𝒫 𝑥 ∈ 𝑈))
14		eleq2 2878	. . . . . 6 ⊢ (𝑤 = 𝑈 → ({𝑥, 𝑦} ∈ 𝑤 ↔ {𝑥, 𝑦} ∈ 𝑈))
15	14	raleqbi1dv 3356	. . . . 5 ⊢ (𝑤 = 𝑈 → (∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤 ↔ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))
16	12, 13, 15	3anbi123d 1433	. . . 4 ⊢ (𝑤 = 𝑈 → ((∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤) ↔ (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈)))
17	16	raleqbi1dv 3356	. . 3 ⊢ (𝑤 = 𝑈 → (∀𝑥 ∈ 𝑤 (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤) ↔ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈)))
18	10, 11, 17	3anbi123d 1433	. 2 ⊢ (𝑤 = 𝑈 → ((Tr 𝑤 ∧ 𝑤 ≠ ∅ ∧ ∀𝑥 ∈ 𝑤 (∪ 𝑥 ∈ 𝑤 ∧ 𝒫 𝑥 ∈ 𝑤 ∧ ∀𝑦 ∈ 𝑤 {𝑥, 𝑦} ∈ 𝑤)) ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))))
19		df-wun 10113	. 2 ⊢ WUni = {𝑧 ∣ (Tr 𝑧 ∧ 𝑧 ≠ ∅ ∧ ∀𝑥 ∈ 𝑧 (∪ 𝑥 ∈ 𝑧 ∧ 𝒫 𝑥 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 {𝑥, 𝑦} ∈ 𝑧))}
20	9, 18, 19	elab2gw 3613	1 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∅c0 4243  𝒫 cpw 4497  {cpr 4527  ∪ cuni 4800  Tr wtr 5136  WUnicwun 10111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-tr 5137  df-wun 10113

This theorem is referenced by:  wuntr  10116  wununi  10117  wunpw  10118  wunpr  10120  wun0  10129  intwun  10146  r1limwun  10147  wunex2  10149  tskwun  10195  gruwun  10224  pwinfi2  40261