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	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ∈𝑔 𝐽 ) = ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ )

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( 𝐼 ∈𝑔 𝐽 ) = ( ∈𝑔 ‘ ⟨ 𝐼 , 𝐽 ⟩ )
2		df-goel	⊢ ∈𝑔 = ( 𝑥 ∈ ( ω × ω ) ↦ ⟨ ∅ , 𝑥 ⟩ )
3	2	a1i	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ∈𝑔 = ( 𝑥 ∈ ( ω × ω ) ↦ ⟨ ∅ , 𝑥 ⟩ ) )
4		opeq2	⊢ ( 𝑥 = ⟨ 𝐼 , 𝐽 ⟩ → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ )
5	4	adantl	⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ 𝑥 = ⟨ 𝐼 , 𝐽 ⟩ ) → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ )
6		opelxpi	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ⟨ 𝐼 , 𝐽 ⟩ ∈ ( ω × ω ) )
7		opex	⊢ ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ ∈ V
8	7	a1i	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ ∈ V )
9	3 5 6 8	fvmptd	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( ∈𝑔 ‘ ⟨ 𝐼 , 𝐽 ⟩ ) = ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ )
10	1 9	syl5eq	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ∈𝑔 𝐽 ) = ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ )