This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Mario Carneiro Godel-sets of formulas - part 2 df-gobi
Description: Define the Godel-set of equivalence. Here the arguments U and V
are also Godel-sets corresponding to smaller formulas. Note that this
is aclass expression, not a wff. (Contributed by Mario Carneiro , 14-Jul-2013)
Ref
Expression
Assertion
df-gobi ⊢ ↔𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( 𝑢 →𝑔 𝑣 ) ∧𝑔 ( 𝑣 →𝑔 𝑢 ) ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cgob ⊢ ↔𝑔
1
vu ⊢ 𝑢
2
cvv ⊢ V
3
vv ⊢ 𝑣
4
1
cv ⊢ 𝑢
5
cgoi ⊢ →𝑔
6
3
cv ⊢ 𝑣
7
4 6 5
co ⊢ ( 𝑢 →𝑔 𝑣 )
8
cgoa ⊢ ∧𝑔
9
6 4 5
co ⊢ ( 𝑣 →𝑔 𝑢 )
10
7 9 8
co ⊢ ( ( 𝑢 →𝑔 𝑣 ) ∧𝑔 ( 𝑣 →𝑔 𝑢 ) )
11
1 3 2 2 10
cmpo ⊢ ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( 𝑢 →𝑔 𝑣 ) ∧𝑔 ( 𝑣 →𝑔 𝑢 ) ) )
12
0 11
wceq ⊢ ↔𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( 𝑢 →𝑔 𝑣 ) ∧𝑔 ( 𝑣 →𝑔 𝑢 ) ) )