Metamath Proof Explorer

Theorem elgrug

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

Ref Expression
Assertion elgrug ⊢ U ∈ V → U ∈ Univ ↔ Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U

Proof

Step Hyp Ref Expression
1 treq ⊢ u = U → Tr ⁡ u ↔ Tr ⁡ U
2 eleq2 ⊢ u = U → 𝒫 x ∈ u ↔ 𝒫 x ∈ U
3 eleq2 ⊢ u = U → x y ∈ u ↔ x y ∈ U
4 3 raleqbi1dv ⊢ u = U → ∀ y ∈ u x y ∈ u ↔ ∀ y ∈ U x y ∈ U
5 oveq1 ⊢ u = U → u x = U x
6 eleq2 ⊢ u = U → ⋃ ran ⁡ y ∈ u ↔ ⋃ ran ⁡ y ∈ U
7 5 6 raleqbidv ⊢ u = U → ∀ y ∈ u x ⋃ ran ⁡ y ∈ u ↔ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
8 2 4 7 3anbi123d ⊢ u = U → 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u ↔ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
9 8 raleqbi1dv ⊢ u = U → ∀ x ∈ u 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u ↔ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
10 1 9 anbi12d ⊢ u = U → Tr ⁡ u ∧ ∀ x ∈ u 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u ↔ Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
11 df-gru ⊢ Univ = u | Tr ⁡ u ∧ ∀ x ∈ u 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u
12 10 11 elab2g ⊢ U ∈ V → U ∈ Univ ↔ Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U