Metamath Proof Explorer


Theorem ismgmOLD

Description: Obsolete version of ismgm as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis ismgmOLD.1 𝑋 = dom dom 𝐺
Assertion ismgmOLD ( 𝐺𝐴 → ( 𝐺 ∈ Magma ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ismgmOLD.1 𝑋 = dom dom 𝐺
2 feq1 ( 𝑔 = 𝐺 → ( 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) )
3 2 exbidv ( 𝑔 = 𝐺 → ( ∃ 𝑡 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ↔ ∃ 𝑡 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) )
4 df-mgmOLD Magma = { 𝑔 ∣ ∃ 𝑡 𝑔 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 }
5 3 4 elab2g ( 𝐺𝐴 → ( 𝐺 ∈ Magma ↔ ∃ 𝑡 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) )
6 f00 ( 𝐺 : ( ∅ × ∅ ) ⟶ ∅ ↔ ( 𝐺 = ∅ ∧ ( ∅ × ∅ ) = ∅ ) )
7 dmeq ( 𝐺 = ∅ → dom 𝐺 = dom ∅ )
8 dmeq ( dom 𝐺 = dom ∅ → dom dom 𝐺 = dom dom ∅ )
9 dm0 dom ∅ = ∅
10 9 dmeqi dom dom ∅ = dom ∅
11 10 9 eqtri dom dom ∅ = ∅
12 8 11 eqtr2di ( dom 𝐺 = dom ∅ → ∅ = dom dom 𝐺 )
13 7 12 syl ( 𝐺 = ∅ → ∅ = dom dom 𝐺 )
14 13 adantr ( ( 𝐺 = ∅ ∧ ( ∅ × ∅ ) = ∅ ) → ∅ = dom dom 𝐺 )
15 6 14 sylbi ( 𝐺 : ( ∅ × ∅ ) ⟶ ∅ → ∅ = dom dom 𝐺 )
16 xpeq12 ( ( 𝑡 = ∅ ∧ 𝑡 = ∅ ) → ( 𝑡 × 𝑡 ) = ( ∅ × ∅ ) )
17 16 anidms ( 𝑡 = ∅ → ( 𝑡 × 𝑡 ) = ( ∅ × ∅ ) )
18 feq23 ( ( ( 𝑡 × 𝑡 ) = ( ∅ × ∅ ) ∧ 𝑡 = ∅ ) → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝐺 : ( ∅ × ∅ ) ⟶ ∅ ) )
19 17 18 mpancom ( 𝑡 = ∅ → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝐺 : ( ∅ × ∅ ) ⟶ ∅ ) )
20 eqeq1 ( 𝑡 = ∅ → ( 𝑡 = dom dom 𝐺 ↔ ∅ = dom dom 𝐺 ) )
21 19 20 imbi12d ( 𝑡 = ∅ → ( ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝑡 = dom dom 𝐺 ) ↔ ( 𝐺 : ( ∅ × ∅ ) ⟶ ∅ → ∅ = dom dom 𝐺 ) ) )
22 15 21 mpbiri ( 𝑡 = ∅ → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝑡 = dom dom 𝐺 ) )
23 fdm ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 → dom 𝐺 = ( 𝑡 × 𝑡 ) )
24 dmeq ( dom 𝐺 = ( 𝑡 × 𝑡 ) → dom dom 𝐺 = dom ( 𝑡 × 𝑡 ) )
25 df-ne ( 𝑡 ≠ ∅ ↔ ¬ 𝑡 = ∅ )
26 dmxp ( 𝑡 ≠ ∅ → dom ( 𝑡 × 𝑡 ) = 𝑡 )
27 25 26 sylbir ( ¬ 𝑡 = ∅ → dom ( 𝑡 × 𝑡 ) = 𝑡 )
28 27 eqeq1d ( ¬ 𝑡 = ∅ → ( dom ( 𝑡 × 𝑡 ) = dom dom 𝐺𝑡 = dom dom 𝐺 ) )
29 28 biimpcd ( dom ( 𝑡 × 𝑡 ) = dom dom 𝐺 → ( ¬ 𝑡 = ∅ → 𝑡 = dom dom 𝐺 ) )
30 29 eqcoms ( dom dom 𝐺 = dom ( 𝑡 × 𝑡 ) → ( ¬ 𝑡 = ∅ → 𝑡 = dom dom 𝐺 ) )
31 23 24 30 3syl ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 → ( ¬ 𝑡 = ∅ → 𝑡 = dom dom 𝐺 ) )
32 31 com12 ( ¬ 𝑡 = ∅ → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝑡 = dom dom 𝐺 ) )
33 22 32 pm2.61i ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝑡 = dom dom 𝐺 )
34 33 pm4.71ri ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ↔ ( 𝑡 = dom dom 𝐺𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) )
35 34 exbii ( ∃ 𝑡 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ↔ ∃ 𝑡 ( 𝑡 = dom dom 𝐺𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) )
36 5 35 syl6bb ( 𝐺𝐴 → ( 𝐺 ∈ Magma ↔ ∃ 𝑡 ( 𝑡 = dom dom 𝐺𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) ) )
37 dmexg ( 𝐺𝐴 → dom 𝐺 ∈ V )
38 dmexg ( dom 𝐺 ∈ V → dom dom 𝐺 ∈ V )
39 xpeq12 ( ( 𝑡 = dom dom 𝐺𝑡 = dom dom 𝐺 ) → ( 𝑡 × 𝑡 ) = ( dom dom 𝐺 × dom dom 𝐺 ) )
40 39 anidms ( 𝑡 = dom dom 𝐺 → ( 𝑡 × 𝑡 ) = ( dom dom 𝐺 × dom dom 𝐺 ) )
41 feq23 ( ( ( 𝑡 × 𝑡 ) = ( dom dom 𝐺 × dom dom 𝐺 ) ∧ 𝑡 = dom dom 𝐺 ) → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) ⟶ dom dom 𝐺 ) )
42 40 41 mpancom ( 𝑡 = dom dom 𝐺 → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) ⟶ dom dom 𝐺 ) )
43 1 eqcomi dom dom 𝐺 = 𝑋
44 43 43 xpeq12i ( dom dom 𝐺 × dom dom 𝐺 ) = ( 𝑋 × 𝑋 )
45 44 43 feq23i ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) ⟶ dom dom 𝐺𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
46 42 45 syl6bb ( 𝑡 = dom dom 𝐺 → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
47 46 ceqsexgv ( dom dom 𝐺 ∈ V → ( ∃ 𝑡 ( 𝑡 = dom dom 𝐺𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
48 37 38 47 3syl ( 𝐺𝐴 → ( ∃ 𝑡 ( 𝑡 = dom dom 𝐺𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
49 36 48 bitrd ( 𝐺𝐴 → ( 𝐺 ∈ Magma ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )