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	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ∈𝑔 𝐽 ) ∈ ( ω × ( ω × ω ) ) )

Proof

Step	Hyp	Ref	Expression
1		goel	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ∈𝑔 𝐽 ) = ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ )
2		peano1	⊢ ∅ ∈ ω
3	2	a1i	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ∅ ∈ ω )
4		opelxpi	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ⟨ 𝐼 , 𝐽 ⟩ ∈ ( ω × ω ) )
5	3 4	opelxpd	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ ∈ ( ω × ( ω × ω ) ) )
6	1 5	eqeltrd	⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ∈𝑔 𝐽 ) ∈ ( ω × ( ω × ω ) ) )