Theorem iswun

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

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

Proof

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