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 >. >. )