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 ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )