gruop

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

		Ref	Expression
	Assertion	gruop	$⊢ (U \in Univ \land A \in U \land B \in U) \to ⟨A, B⟩ \in U$

Step	Hyp	Ref	Expression
1		dfopg	$⊢ (A \in U \land B \in U) \to ⟨A, B⟩ = \{\{A\}, \{A, B\}\}$
2	1	3adant1	$⊢ (U \in Univ \land A \in U \land B \in U) \to ⟨A, B⟩ = \{\{A\}, \{A, B\}\}$
3		simp1	$⊢ (U \in Univ \land A \in U \land B \in U) \to U \in Univ$
4		grusn	$⊢ (U \in Univ \land A \in U) \to \{A\} \in U$
5	4	3adant3	$⊢ (U \in Univ \land A \in U \land B \in U) \to \{A\} \in U$
6		grupr	$⊢ (U \in Univ \land A \in U \land B \in U) \to \{A, B\} \in U$
7		grupr	$⊢ (U \in Univ \land \{A\} \in U \land \{A, B\} \in U) \to \{\{A\}, \{A, B\}\} \in U$
8	3 5 6 7	syl3anc	$⊢ (U \in Univ \land A \in U \land B \in U) \to \{\{A\}, \{A, B\}\} \in U$
9	2 8	eqeltrd	$⊢ (U \in Univ \land A \in U \land B \in U) \to ⟨A, B⟩ \in U$

Metamath Proof Explorer