Definition df-muc 6103

Description: Define cardinal multiplication. Definition from [Rosser] p. 378. (Contributed by Scott Fenton, 24-Feb-2015.)

Assertion

Ref	Expression
df-muc	⊢ ·c = (m ∈ NC , n ∈ NC ↦ {a ∣ ∃b ∈ m ∃g ∈ n a ≈ (b × g)})

Distinct variable group:   m,n,a,b,g

Detailed syntax breakdown of Definition df-muc

Step	Hyp	Ref	Expression
1		cmuc 6093	. 2 class ·c
2		vm	. . 3 setvar m
3		vn	. . 3 setvar n
4		cncs 6089	. . 3 class NC
5		va	. . . . . . . 8 setvar a
6	5	cv 1641	. . . . . . 7 class a
7		vb	. . . . . . . . 9 setvar b
8	7	cv 1641	. . . . . . . 8 class b
9		vg	. . . . . . . . 9 setvar g
10	9	cv 1641	. . . . . . . 8 class g
11	8, 10	cxp 4771	. . . . . . 7 class (b × g)
12		cen 6029	. . . . . . 7 class ≈
13	6, 11, 12	wbr 4640	. . . . . 6 wff a ≈ (b × g)
14	3	cv 1641	. . . . . 6 class n
15	13, 9, 14	wrex 2616	. . . . 5 wff ∃g ∈ n a ≈ (b × g)
16	2	cv 1641	. . . . 5 class m
17	15, 7, 16	wrex 2616	. . . 4 wff ∃b ∈ m ∃g ∈ n a ≈ (b × g)
18	17, 5	cab 2339	. . 3 class {a ∣ ∃b ∈ m ∃g ∈ n a ≈ (b × g)}
19	2, 3, 4, 4, 18	cmpt2 5654	. 2 class (m ∈ NC , n ∈ NC ↦ {a ∣ ∃b ∈ m ∃g ∈ n a ≈ (b × g)})
20	1, 19	wceq 1642	1 wff ·c = (m ∈ NC , n ∈ NC ↦ {a ∣ ∃b ∈ m ∃g ∈ n a ≈ (b × g)})

This definition is referenced by:  ovmuc  6131  mucex  6134