Theorem goelel3xp

Description: A "Godel-set of membership" is a member of a doubled Cartesian product. (Contributed by AV, 16-Sep-2023)

	Ref	Expression
Assertion	goelel3xp	|- ( ( I e. _om /\ J e. _om ) -> ( I e.g J ) e. ( _om X. ( _om X. _om ) ) )

Proof

Step	Hyp	Ref	Expression
1		goel	|- ( ( I e. _om /\ J e. _om ) -> ( I e.g J ) = <. (/) , <. I , J >. >. )
2		peano1	|- (/) e. _om
3	2	a1i	|- ( ( I e. _om /\ J e. _om ) -> (/) e. _om )
4		opelxpi	|- ( ( I e. _om /\ J e. _om ) -> <. I , J >. e. ( _om X. _om ) )
5	3 4	opelxpd	|- ( ( I e. _om /\ J e. _om ) -> <. (/) , <. I , J >. >. e. ( _om X. ( _om X. _om ) ) )
6	1 5	eqeltrd	|- ( ( I e. _om /\ J e. _om ) -> ( I e.g J ) e. ( _om X. ( _om X. _om ) ) )