Metamath Proof Explorer

Theorem gruop

Description: A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 dfopg ⊢ A ∈ U ∧ B ∈ U → A B = A A B
2 1 3adant1 ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A B = A A B
3 simp1 ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → U ∈ Univ
4 grusn ⊢ U ∈ Univ ∧ A ∈ U → A ∈ U
5 4 3adant3 ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A ∈ U
6 grupr ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A B ∈ U
7 grupr ⊢ U ∈ Univ ∧ A ∈ U ∧ A B ∈ U → A A B ∈ U
8 3 5 6 7 syl3anc ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A A B ∈ U
9 2 8 eqeltrd ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A B ∈ U