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	⊢ =_𝑔 = ( 𝑢 ∈ ω , 𝑣 ∈ ω ↦ ⦋ suc ( 𝑢 ∪ 𝑣 ) / 𝑤 ⦌ ∀_𝑔 𝑤 ( ( 𝑤 ∈_𝑔 𝑢 ) ↔_𝑔 ( 𝑤 ∈_𝑔 𝑣 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgoq	⊢ =_𝑔
1		vu	⊢ 𝑢
2		com	⊢ ω
3		vv	⊢ 𝑣
4	1	cv	⊢ 𝑢
5	3	cv	⊢ 𝑣
6	4 5	cun	⊢ ( 𝑢 ∪ 𝑣 )
7	6	csuc	⊢ suc ( 𝑢 ∪ 𝑣 )
8		vw	⊢ 𝑤
9	8	cv	⊢ 𝑤
10		cgoe	⊢ ∈_𝑔
11	9 4 10	co	⊢ ( 𝑤 ∈_𝑔 𝑢 )
12		cgob	⊢ ↔_𝑔
13	9 5 10	co	⊢ ( 𝑤 ∈_𝑔 𝑣 )
14	11 13 12	co	⊢ ( ( 𝑤 ∈_𝑔 𝑢 ) ↔_𝑔 ( 𝑤 ∈_𝑔 𝑣 ) )
15	14 9	cgol	⊢ ∀_𝑔 𝑤 ( ( 𝑤 ∈_𝑔 𝑢 ) ↔_𝑔 ( 𝑤 ∈_𝑔 𝑣 ) )
16	8 7 15	csb	⊢ ⦋ suc ( 𝑢 ∪ 𝑣 ) / 𝑤 ⦌ ∀_𝑔 𝑤 ( ( 𝑤 ∈_𝑔 𝑢 ) ↔_𝑔 ( 𝑤 ∈_𝑔 𝑣 ) )
17	1 3 2 2 16	cmpo	⊢ ( 𝑢 ∈ ω , 𝑣 ∈ ω ↦ ⦋ suc ( 𝑢 ∪ 𝑣 ) / 𝑤 ⦌ ∀_𝑔 𝑤 ( ( 𝑤 ∈_𝑔 𝑢 ) ↔_𝑔 ( 𝑤 ∈_𝑔 𝑣 ) ) )
18	0 17	wceq	⊢ =_𝑔 = ( 𝑢 ∈ ω , 𝑣 ∈ ω ↦ ⦋ suc ( 𝑢 ∪ 𝑣 ) / 𝑤 ⦌ ∀_𝑔 𝑤 ( ( 𝑤 ∈_𝑔 𝑢 ) ↔_𝑔 ( 𝑤 ∈_𝑔 𝑣 ) ) )

Metamath Proof Explorer

Definition df-goeq

Detailed syntax breakdown