Metamath Proof Explorer


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 ω J ω I 𝑔 J ω × ω × ω

Proof

Step Hyp Ref Expression
1 goel I ω J ω I 𝑔 J = I J
2 peano1 ω
3 2 a1i I ω J ω ω
4 opelxpi I ω J ω I J ω × ω
5 3 4 opelxpd I ω J ω I J ω × ω × ω
6 1 5 eqeltrd I ω J ω I 𝑔 J ω × ω × ω