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

Metamath Proof Explorer

Definition df-exid

Description: A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.)

Ref Expression
Assertion df-exid ExId = { 𝑔 ∣ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cexid ⊢ ExId
1 vg ⊢ 𝑔
2 vx ⊢ 𝑥
3 1 cv ⊢ 𝑔
4 3 cdm ⊢ dom 𝑔
5 4 cdm ⊢ dom dom 𝑔
6 vy ⊢ 𝑦
7 2 cv ⊢ 𝑥
8 6 cv ⊢ 𝑦
9 7 8 3 co ⊢ ( 𝑥 𝑔 𝑦 )
10 9 8 wceq ⊢ ( 𝑥 𝑔 𝑦 ) = 𝑦
11 8 7 3 co ⊢ ( 𝑦 𝑔 𝑥 )
12 11 8 wceq ⊢ ( 𝑦 𝑔 𝑥 ) = 𝑦
13 10 12 wa ⊢ ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 )
14 13 6 5 wral ⊢ ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 )
15 14 2 5 wrex ⊢ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 )
16 15 1 cab ⊢ { 𝑔 ∣ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) }
17 0 16 wceq ⊢ ExId = { 𝑔 ∣ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) }