This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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