Theorem gruwun

Description: A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	gruwun	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝑈 ∈ WUni )

Proof

Step	Hyp	Ref	Expression
1		grutr	⊢ ( 𝑈 ∈ Univ → Tr 𝑈 )
2	1	adantr	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → Tr 𝑈 )
3		simpr	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝑈 ≠ ∅ )
4		gruuni	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝑈 )
5	4	adantlr	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝑈 )
6		grupw	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ) → 𝒫 𝑥 ∈ 𝑈 )
7	6	adantlr	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → 𝒫 𝑥 ∈ 𝑈 )
8		grupr	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → { 𝑥 , 𝑦 } ∈ 𝑈 )
9	8	ad4ant134	⊢ ( ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝑈 ) → { 𝑥 , 𝑦 } ∈ 𝑈 )
10	9	ralrimiva	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 )
11	5 7 10	3jca	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) )
12	11	ralrimiva	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) )
13		iswun	⊢ ( 𝑈 ∈ Univ → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )
14	13	adantr	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )
15	2 3 12 14	mpbir3and	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑈 ≠ ∅ ) → 𝑈 ∈ WUni )