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

Metamath Proof Explorer

Definition df-goim

Description: Define the Godel-set of implication. 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-goim →𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑢 ⊼𝑔 ¬𝑔 𝑣 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgoi ⊢ →𝑔
1 vu ⊢ 𝑢
2 cvv ⊢ V
3 vv ⊢ 𝑣
4 1 cv ⊢ 𝑢
5 cgna ⊢ ⊼𝑔
6 3 cv ⊢ 𝑣
7 6 cgon ⊢ ¬𝑔 𝑣
8 4 7 5 co ⊢ ( 𝑢 ⊼𝑔 ¬𝑔 𝑣 )
9 1 3 2 2 8 cmpo ⊢ ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑢 ⊼𝑔 ¬𝑔 𝑣 ) )
10 0 9 wceq ⊢ →𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑢 ⊼𝑔 ¬𝑔 𝑣 ) )