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		df-wun	⊢ WUni = { 𝑢 ∣ ( Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑢 ( ∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ) }
11	9 10	elab2g	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )