# Metamath Proof Explorer

## Theorem opidonOLD

Description: Obsolete version of mndpfo as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis opidonOLD.1 𝑋 = dom dom 𝐺
Assertion opidonOLD ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 )

### Proof

Step Hyp Ref Expression
1 opidonOLD.1 𝑋 = dom dom 𝐺
2 inss1 ( Magma ∩ ExId ) ⊆ Magma
3 2 sseli ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 ∈ Magma )
4 1 ismgmOLD ( 𝐺 ∈ Magma → ( 𝐺 ∈ Magma ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
5 4 ibi ( 𝐺 ∈ Magma → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
6 3 5 syl ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
7 inss2 ( Magma ∩ ExId ) ⊆ ExId
8 7 sseli ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 ∈ ExId )
9 1 isexid ( 𝐺 ∈ ExId → ( 𝐺 ∈ ExId ↔ ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
10 9 biimpd ( 𝐺 ∈ ExId → ( 𝐺 ∈ ExId → ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
11 8 8 10 sylc ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
12 simpl ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
13 12 ralimi ( ∀ 𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
14 oveq2 ( 𝑥 = 𝑦 → ( 𝑢 𝐺 𝑥 ) = ( 𝑢 𝐺 𝑦 ) )
15 id ( 𝑥 = 𝑦𝑥 = 𝑦 )
16 14 15 eqeq12d ( 𝑥 = 𝑦 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑢 𝐺 𝑦 ) = 𝑦 ) )
17 16 rspcv ( 𝑦𝑋 → ( ∀ 𝑥𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 → ( 𝑢 𝐺 𝑦 ) = 𝑦 ) )
18 eqcom ( 𝑦 = ( 𝑢 𝐺 𝑥 ) ↔ ( 𝑢 𝐺 𝑥 ) = 𝑦 )
19 14 eqeq1d ( 𝑥 = 𝑦 → ( ( 𝑢 𝐺 𝑥 ) = 𝑦 ↔ ( 𝑢 𝐺 𝑦 ) = 𝑦 ) )
20 18 19 syl5bb ( 𝑥 = 𝑦 → ( 𝑦 = ( 𝑢 𝐺 𝑥 ) ↔ ( 𝑢 𝐺 𝑦 ) = 𝑦 ) )
21 20 rspcev ( ( 𝑦𝑋 ∧ ( 𝑢 𝐺 𝑦 ) = 𝑦 ) → ∃ 𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) )
22 21 ex ( 𝑦𝑋 → ( ( 𝑢 𝐺 𝑦 ) = 𝑦 → ∃ 𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) ) )
23 17 22 syld ( 𝑦𝑋 → ( ∀ 𝑥𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 → ∃ 𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) ) )
24 13 23 syl5 ( 𝑦𝑋 → ( ∀ 𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∃ 𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) ) )
25 24 reximdv ( 𝑦𝑋 → ( ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∃ 𝑢𝑋𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) ) )
26 25 impcom ( ( ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ 𝑦𝑋 ) → ∃ 𝑢𝑋𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) )
27 26 ralrimiva ( ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑦𝑋𝑢𝑋𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) )
28 11 27 syl ( 𝐺 ∈ ( Magma ∩ ExId ) → ∀ 𝑦𝑋𝑢𝑋𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) )
29 foov ( 𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑦𝑋𝑢𝑋𝑥𝑋 𝑦 = ( 𝑢 𝐺 𝑥 ) ) )
30 6 28 29 sylanbrc ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 )