Metamath Proof Explorer

Theorem goel

Description: A "Godel-set of membership". The variables are identified by their indices (which are natural numbers), and the membership v_i e. v_j is coded as <. (/) , <. i , j >. >. . (Contributed by AV, 15-Sep-2023)

		Ref	Expression
	Assertion	goel	$⊢ (I \in ω \land J \in ω) \to I \in_{𝑔} J = ⟨\emptyset, ⟨I, J⟩⟩$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$⊢ I \in_{𝑔} J = \in_{𝑔} (⟨I, J⟩)$
2		df-goel	$⊢ \in_{𝑔} = (x \in (ω \times ω) ⟼ ⟨\emptyset, x⟩)$
3	2	a1i	$⊢ (I \in ω \land J \in ω) \to \in_{𝑔} = (x \in (ω \times ω) ⟼ ⟨\emptyset, x⟩)$
4		opeq2	$⊢ x = ⟨I, J⟩ \to ⟨\emptyset, x⟩ = ⟨\emptyset, ⟨I, J⟩⟩$
5	4	adantl	$⊢ ((I \in ω \land J \in ω) \land x = ⟨I, J⟩) \to ⟨\emptyset, x⟩ = ⟨\emptyset, ⟨I, J⟩⟩$
6		opelxpi	$⊢ (I \in ω \land J \in ω) \to ⟨I, J⟩ \in (ω \times ω)$
7		opex	$⊢ ⟨\emptyset, ⟨I, J⟩⟩ \in V$
8	7	a1i	$⊢ (I \in ω \land J \in ω) \to ⟨\emptyset, ⟨I, J⟩⟩ \in V$
9	3 5 6 8	fvmptd	$⊢ (I \in ω \land J \in ω) \to \in_{𝑔} (⟨I, J⟩) = ⟨\emptyset, ⟨I, J⟩⟩$
10	1 9	syl5eq	$⊢ (I \in ω \land J \in ω) \to I \in_{𝑔} J = ⟨\emptyset, ⟨I, J⟩⟩$