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