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

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 bitrdi ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ 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 bitrdi ⊢ ( 𝑡 = dom dom 𝐺 → ( 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
47 46 ceqsexgv ⊢ ( dom dom 𝐺 ∈ V → ( ∃ 𝑡 ( 𝑡 = dom dom 𝐺 ∧ 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
48 37 38 47 3syl ⊢ ( 𝐺 ∈ 𝐴 → ( ∃ 𝑡 ( 𝑡 = dom dom 𝐺 ∧ 𝐺 : ( 𝑡 × 𝑡 ) ⟶ 𝑡 ) ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
49 36 48 bitrd ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ Magma ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )