Metamath Proof Explorer


Theorem opidon2OLD

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) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 opidon2OLD.1 𝑋 = ran 𝐺
2 eqid dom dom 𝐺 = dom dom 𝐺
3 2 opidonOLD ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 )
4 forn ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → ran 𝐺 = dom dom 𝐺 )
5 1 4 eqtr2id ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺 → dom dom 𝐺 = 𝑋 )
6 xpeq12 ( ( dom dom 𝐺 = 𝑋 ∧ dom dom 𝐺 = 𝑋 ) → ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) )
7 6 anidms ( dom dom 𝐺 = 𝑋 → ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) )
8 foeq2 ( ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 ) → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺 ) )
9 7 8 syl ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺 ) )
10 foeq3 ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ dom dom 𝐺𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 ) )
11 9 10 bitrd ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 ) )
12 11 biimpd ( dom dom 𝐺 = 𝑋 → ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 ) )
13 5 12 mpcom ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) –onto→ dom dom 𝐺𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 )
14 3 13 syl ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 : ( 𝑋 × 𝑋 ) –onto𝑋 )