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

Metamath Proof Explorer

Theorem isexid

Description: The predicate G has a left and right identity element. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis isexid.1 ⊢ 𝑋 = dom dom 𝐺
Assertion isexid ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ ExId ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 isexid.1 ⊢ 𝑋 = dom dom 𝐺
2 dmeq ⊢ ( 𝑔 = 𝐺 → dom 𝑔 = dom 𝐺 )
3 2 dmeqd ⊢ ( 𝑔 = 𝐺 → dom dom 𝑔 = dom dom 𝐺 )
4 3 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → dom dom 𝑔 = 𝑋 )
5 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
6 5 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ↔ ( 𝑥 𝐺 𝑦 ) = 𝑦 ) )
7 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑦 𝑔 𝑥 ) = ( 𝑦 𝐺 𝑥 ) )
8 7 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑦 𝑔 𝑥 ) = 𝑦 ↔ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) )
9 6 8 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) )
10 4 9 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) )
11 4 10 rexeqbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) )
12 df-exid ⊢ ExId = { 𝑔 ∣ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) }
13 11 12 elab2g ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ ExId ↔ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) )