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⦌∀𝑔ww∈𝑔u↔𝑔w∈𝑔v

Detailed syntax breakdown

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