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