This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem goeleq12bg

Description: Two "Godel-set of membership" codes for two variables are equal iff the two corresponding variables are equal. (Contributed by AV, 8-Oct-2023)

Ref Expression
Assertion goeleq12bg ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ( 𝐼 ∈𝑔 𝐽 ) = ( 𝑀 ∈𝑔 𝑁 ) ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 goel ⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝐼 ∈𝑔 𝐽 ) = ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ )
2 goel ⊢ ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) → ( 𝑀 ∈𝑔 𝑁 ) = ⟨ ∅ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
3 1 2 eqeqan12rd ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ( 𝐼 ∈𝑔 𝐽 ) = ( 𝑀 ∈𝑔 𝑁 ) ↔ ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) )
4 0ex ⊢ ∅ ∈ V
5 opex ⊢ ⟨ 𝐼 , 𝐽 ⟩ ∈ V
6 4 5 opth ⊢ ( ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ↔ ( ∅ = ∅ ∧ ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ) )
7 eqid ⊢ ∅ = ∅
8 7 biantrur ⊢ ( ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ∅ = ∅ ∧ ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ) )
9 opthg ⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )
10 9 adantl ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )
11 8 10 bitr3id ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ( ∅ = ∅ ∧ ⟨ 𝐼 , 𝐽 ⟩ = ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )
12 6 11 bitrid ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ⟨ ∅ , ⟨ 𝐼 , 𝐽 ⟩ ⟩ = ⟨ ∅ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )
13 3 12 bitrd ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑁 ∈ ω ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ) → ( ( 𝐼 ∈𝑔 𝐽 ) = ( 𝑀 ∈𝑔 𝑁 ) ↔ ( 𝐼 = 𝑀 ∧ 𝐽 = 𝑁 ) ) )