Theorem elgrug

Description: Properties of a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	elgrug	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ Univ ↔ ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		treq	⊢ ( 𝑢 = 𝑈 → ( Tr 𝑢 ↔ Tr 𝑈 ) )
2		eleq2	⊢ ( 𝑢 = 𝑈 → ( 𝒫 𝑥 ∈ 𝑢 ↔ 𝒫 𝑥 ∈ 𝑈 ) )
3		eleq2	⊢ ( 𝑢 = 𝑈 → ( { 𝑥 , 𝑦 } ∈ 𝑢 ↔ { 𝑥 , 𝑦 } ∈ 𝑈 ) )
4	3	raleqbi1dv	⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ↔ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) )
5		oveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ↑m 𝑥 ) = ( 𝑈 ↑m 𝑥 ) )
6		eleq2	⊢ ( 𝑢 = 𝑈 → ( ∪ ran 𝑦 ∈ 𝑢 ↔ ∪ ran 𝑦 ∈ 𝑈 ) )
7	5 6	raleqbidv	⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ↔ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) )
8	2 4 7	3anbi123d	⊢ ( 𝑢 = 𝑈 → ( ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ↔ ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) )
9	8	raleqbi1dv	⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ↔ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) )
10	1 9	anbi12d	⊢ ( 𝑢 = 𝑈 → ( ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) ↔ ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) ) )
11		df-gru	⊢ Univ = { 𝑢 ∣ ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) }
12	10 11	elab2g	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ Univ ↔ ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) ) )