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

Metamath Proof Explorer

Definition df-goeq

Description: Define the Godel-set of equality. Here the arguments x = <. N , P >. correspond to v_N and v_P , so ( (/) =g 1o ) actually means v_0 = v_1 , not 0 = 1 . Here we use the trick mentioned in ax-ext to introduce equality as a defined notion in terms of e.g . The expression suc ( u u. v ) = max ( u , v ) + 1 here is a convenient way of getting a dummy variable distinct from u and v . (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-goeq ⊢ = 𝑔 = u ∈ ω , v ∈ ω ⟼ ⦋ suc ⁡ u ∪ v / w⦌ ∀ 𝑔 w w ∈ 𝑔 u ↔ 𝑔 w ∈ 𝑔 v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgoq class = 𝑔
1 vu setvar u
2 com class ω
3 vv setvar v
4 1 cv setvar u
5 3 cv setvar v
6 4 5 cun class u ∪ v
7 6 csuc class suc ⁡ u ∪ v
8 vw setvar w
9 8 cv setvar w
10 cgoe class ∈ 𝑔
11 9 4 10 co class w ∈ 𝑔 u
12 cgob class ↔ 𝑔
13 9 5 10 co class w ∈ 𝑔 v
14 11 13 12 co class w ∈ 𝑔 u ↔ 𝑔 w ∈ 𝑔 v
15 14 9 cgol class ∀ 𝑔 w w ∈ 𝑔 u ↔ 𝑔 w ∈ 𝑔 v
16 8 7 15 csb class ⦋ suc ⁡ u ∪ v / w⦌ ∀ 𝑔 w w ∈ 𝑔 u ↔ 𝑔 w ∈ 𝑔 v
17 1 3 2 2 16 cmpo class u ∈ ω , v ∈ ω ⟼ ⦋ suc ⁡ u ∪ v / w⦌ ∀ 𝑔 w w ∈ 𝑔 u ↔ 𝑔 w ∈ 𝑔 v
18 0 17 wceq wff = 𝑔 = u ∈ ω , v ∈ ω ⟼ ⦋ suc ⁡ u ∪ v / w⦌ ∀ 𝑔 w w ∈ 𝑔 u ↔ 𝑔 w ∈ 𝑔 v