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 e. _om /\ J e. _om ) -> ( I e.g J ) = <. (/) , <. I , J >. >. )

Proof

Step Hyp Ref Expression
1 df-ov
 |-  ( I e.g J ) = ( e.g ` <. I , J >. )
2 df-goel
 |-  e.g = ( x e. ( _om X. _om ) |-> <. (/) , x >. )
3 2 a1i
 |-  ( ( I e. _om /\ J e. _om ) -> e.g = ( x e. ( _om X. _om ) |-> <. (/) , x >. ) )
4 opeq2
 |-  ( x = <. I , J >. -> <. (/) , x >. = <. (/) , <. I , J >. >. )
5 4 adantl
 |-  ( ( ( I e. _om /\ J e. _om ) /\ x = <. I , J >. ) -> <. (/) , x >. = <. (/) , <. I , J >. >. )
6 opelxpi
 |-  ( ( I e. _om /\ J e. _om ) -> <. I , J >. e. ( _om X. _om ) )
7 opex
 |-  <. (/) , <. I , J >. >. e. _V
8 7 a1i
 |-  ( ( I e. _om /\ J e. _om ) -> <. (/) , <. I , J >. >. e. _V )
9 3 5 6 8 fvmptd
 |-  ( ( I e. _om /\ J e. _om ) -> ( e.g ` <. I , J >. ) = <. (/) , <. I , J >. >. )
10 1 9 syl5eq
 |-  ( ( I e. _om /\ J e. _om ) -> ( I e.g J ) = <. (/) , <. I , J >. >. )