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 ⊢X=dom⁡dom⁡G
Assertion opidonOLD ⊢G∈Magma∩ExId→G:X×X⟶ontoX

Proof

Step Hyp Ref Expression
1 opidonOLD.1 ⊢X=dom⁡dom⁡G
2 inss1 ⊢Magma∩ExId⊆Magma
3 2 sseli ⊢G∈Magma∩ExId→G∈Magma
4 1 ismgmOLD ⊢G∈Magma→G∈Magma↔G:X×X⟶X
5 4 ibi ⊢G∈Magma→G:X×X⟶X
6 3 5 syl ⊢G∈Magma∩ExId→G:X×X⟶X
7 inss2 ⊢Magma∩ExId⊆ExId
8 7 sseli ⊢G∈Magma∩ExId→G∈ExId
9 1 isexid ⊢G∈ExId→G∈ExId↔∃u∈X∀x∈XuGx=x∧xGu=x
10 9 biimpd ⊢G∈ExId→G∈ExId→∃u∈X∀x∈XuGx=x∧xGu=x
11 8 8 10 sylc ⊢G∈Magma∩ExId→∃u∈X∀x∈XuGx=x∧xGu=x
12 simpl ⊢uGx=x∧xGu=x→uGx=x
13 12 ralimi ⊢∀x∈XuGx=x∧xGu=x→∀x∈XuGx=x
14 oveq2 ⊢x=y→uGx=uGy
15 id ⊢x=y→x=y
16 14 15 eqeq12d ⊢x=y→uGx=x↔uGy=y
17 16 rspcv ⊢y∈X→∀x∈XuGx=x→uGy=y
18 eqcom ⊢y=uGx↔uGx=y
19 14 eqeq1d ⊢x=y→uGx=y↔uGy=y
20 18 19 bitrid ⊢x=y→y=uGx↔uGy=y
21 20 rspcev ⊢y∈X∧uGy=y→∃x∈Xy=uGx
22 21 ex ⊢y∈X→uGy=y→∃x∈Xy=uGx
23 17 22 syld ⊢y∈X→∀x∈XuGx=x→∃x∈Xy=uGx
24 13 23 syl5 ⊢y∈X→∀x∈XuGx=x∧xGu=x→∃x∈Xy=uGx
25 24 reximdv ⊢y∈X→∃u∈X∀x∈XuGx=x∧xGu=x→∃u∈X∃x∈Xy=uGx
26 25 impcom ⊢∃u∈X∀x∈XuGx=x∧xGu=x∧y∈X→∃u∈X∃x∈Xy=uGx
27 26 ralrimiva ⊢∃u∈X∀x∈XuGx=x∧xGu=x→∀y∈X∃u∈X∃x∈Xy=uGx
28 11 27 syl ⊢G∈Magma∩ExId→∀y∈X∃u∈X∃x∈Xy=uGx
29 foov ⊢G:X×X⟶ontoX↔G:X×X⟶X∧∀y∈X∃u∈X∃x∈Xy=uGx
30 6 28 29 sylanbrc ⊢G∈Magma∩ExId→G:X×X⟶ontoX