goelel3xp

Description: A "Godel-set of membership" is a member of a doubled Cartesian product. (Contributed by AV, 16-Sep-2023)

		Ref	Expression
	Assertion	goelel3xp	$⊢ (I \in ω \land J \in ω) \to I \in_{𝑔} J \in (ω \times (ω \times ω))$

Step	Hyp	Ref	Expression
1		goel	$⊢ (I \in ω \land J \in ω) \to I \in_{𝑔} J = ⟨\emptyset, ⟨I, J⟩⟩$
2		peano1	$⊢ \emptyset \in ω$
3	2	a1i	$⊢ (I \in ω \land J \in ω) \to \emptyset \in ω$
4		opelxpi	$⊢ (I \in ω \land J \in ω) \to ⟨I, J⟩ \in (ω \times ω)$
5	3 4	opelxpd	$⊢ (I \in ω \land J \in ω) \to ⟨\emptyset, ⟨I, J⟩⟩ \in (ω \times (ω \times ω))$
6	1 5	eqeltrd	$⊢ (I \in ω \land J \in ω) \to I \in_{𝑔} J \in (ω \times (ω \times ω))$

Metamath Proof Explorer