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

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→ 𝑋 )