Definition df-goeq 33406

Description: Define the Godel-set of equality. Here the arguments 𝑥 = ⟨𝑁, 𝑃⟩ correspond to v_N and v_P , so (∅=_𝑔1_o) actually means v₀ = v₁ , not 0 = 1. Here we use the trick mentioned in ax-ext 2709 to introduce equality as a defined notion in terms of ∈_𝑔. The expression suc (𝑢 ∪ 𝑣) = max (𝑢, 𝑣) + 1 here is a convenient way of getting a dummy variable distinct from 𝑢 and 𝑣. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-goeq	⊢ =𝑔 = (𝑢 ∈ ω, 𝑣 ∈ ω ↦ ⦋suc (𝑢 ∪ 𝑣) / 𝑤⦌∀𝑔𝑤((𝑤∈𝑔𝑢) ↔𝑔 (𝑤∈𝑔𝑣)))

Distinct variable group:   𝑣,𝑢,𝑤

Detailed syntax breakdown of Definition df-goeq

Step	Hyp	Ref	Expression
1		cgoq 33399	. 2 class =𝑔
2		vu	. . 3 setvar 𝑢
3		vv	. . 3 setvar 𝑣
4		com 7712	. . 3 class ω
5		vw	. . . 4 setvar 𝑤
6	2	cv 1538	. . . . . 6 class 𝑢
7	3	cv 1538	. . . . . 6 class 𝑣
8	6, 7	cun 3885	. . . . 5 class (𝑢 ∪ 𝑣)
9	8	csuc 6268	. . . 4 class suc (𝑢 ∪ 𝑣)
10	5	cv 1538	. . . . . . 7 class 𝑤
11		cgoe 33295	. . . . . . 7 class ∈𝑔
12	10, 6, 11	co 7275	. . . . . 6 class (𝑤∈𝑔𝑢)
13	10, 7, 11	co 7275	. . . . . 6 class (𝑤∈𝑔𝑣)
14		cgob 33398	. . . . . 6 class ↔𝑔
15	12, 13, 14	co 7275	. . . . 5 class ((𝑤∈𝑔𝑢) ↔𝑔 (𝑤∈𝑔𝑣))
16	15, 10	cgol 33297	. . . 4 class ∀𝑔𝑤((𝑤∈𝑔𝑢) ↔𝑔 (𝑤∈𝑔𝑣))
17	5, 9, 16	csb 3832	. . 3 class ⦋suc (𝑢 ∪ 𝑣) / 𝑤⦌∀𝑔𝑤((𝑤∈𝑔𝑢) ↔𝑔 (𝑤∈𝑔𝑣))
18	2, 3, 4, 4, 17	cmpo 7277	. 2 class (𝑢 ∈ ω, 𝑣 ∈ ω ↦ ⦋suc (𝑢 ∪ 𝑣) / 𝑤⦌∀𝑔𝑤((𝑤∈𝑔𝑢) ↔𝑔 (𝑤∈𝑔𝑣)))
19	1, 18	wceq 1539	1 wff =𝑔 = (𝑢 ∈ ω, 𝑣 ∈ ω ↦ ⦋suc (𝑢 ∪ 𝑣) / 𝑤⦌∀𝑔𝑤((𝑤∈𝑔𝑢) ↔𝑔 (𝑤∈𝑔𝑣)))

This definition is referenced by: (None)