Theorem gruop

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

	Ref	Expression
Assertion	gruop	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		dfopg	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
2	1	3adant1	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
3		simp1	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → 𝑈 ∈ Univ )
4		grusn	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → { 𝐴 } ∈ 𝑈 )
5	4	3adant3	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → { 𝐴 } ∈ 𝑈 )
6		grupr	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → { 𝐴 , 𝐵 } ∈ 𝑈 )
7		grupr	⊢ ( ( 𝑈 ∈ Univ ∧ { 𝐴 } ∈ 𝑈 ∧ { 𝐴 , 𝐵 } ∈ 𝑈 ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ 𝑈 )
8	3 5 6 7	syl3anc	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ 𝑈 )
9	2 8	eqeltrd	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑈 )