Metamath Proof Explorer

Theorem grupr

Description: A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion grupr ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A B ∈ U

Proof

Step Hyp Ref Expression
1 elgrug ⊢ U ∈ Univ → U ∈ Univ ↔ Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
2 1 ibi ⊢ U ∈ Univ → Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
3 2 simprd ⊢ U ∈ Univ → ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
4 preq2 ⊢ y = B → x y = x B
5 4 eleq1d ⊢ y = B → x y ∈ U ↔ x B ∈ U
6 5 rspccv ⊢ ∀ y ∈ U x y ∈ U → B ∈ U → x B ∈ U
7 6 3ad2ant2 ⊢ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U → B ∈ U → x B ∈ U
8 7 com12 ⊢ B ∈ U → 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U → x B ∈ U
9 8 ralimdv ⊢ B ∈ U → ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U → ∀ x ∈ U x B ∈ U
10 3 9 syl5com ⊢ U ∈ Univ → B ∈ U → ∀ x ∈ U x B ∈ U
11 preq1 ⊢ x = A → x B = A B
12 11 eleq1d ⊢ x = A → x B ∈ U ↔ A B ∈ U
13 12 rspccv ⊢ ∀ x ∈ U x B ∈ U → A ∈ U → A B ∈ U
14 10 13 syl6 ⊢ U ∈ Univ → B ∈ U → A ∈ U → A B ∈ U
15 14 com23 ⊢ U ∈ Univ → A ∈ U → B ∈ U → A B ∈ U
16 15 3imp ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A B ∈ U