# Metamath Proof Explorer

## 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 𝑦𝑈 ) ) ) )