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 bitrid ⊢ ( 𝑥 = 𝑦 → ( 𝑦 = ( 𝑢 𝐺 𝑥 ) ↔ ( 𝑢 𝐺 𝑦 ) = 𝑦 ) )
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→ 𝑋 )