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

Metamath Proof Explorer

Definition df-co

Description: Define the composition of two classes. Definition 6.6(3) of TakeutiZaring p. 24. For example, ( ( exp o. cos )0 ) =e ( ex-co ) because ( cos0 ) = 1 (see cos0 ) and ( exp1 ) = e (see df-e ). Note that Definition 7 of Suppes p. 63 reverses A and B , uses /. instead of o. , and calls the operation "relative product". (Contributed by NM, 4-Jul-1994)

Ref Expression
Assertion df-co ⊢ A ∘ B = x y | ∃ z x B z ∧ z A y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cB class B
2 0 1 ccom class A ∘ B
3 vx setvar x
4 vy setvar y
5 vz setvar z
6 3 cv setvar x
7 5 cv setvar z
8 6 7 1 wbr wff x B z
9 4 cv setvar y
10 7 9 0 wbr wff z A y
11 8 10 wa wff x B z ∧ z A y
12 11 5 wex wff ∃ z x B z ∧ z A y
13 12 3 4 copab class x y | ∃ z x B z ∧ z A y
14 2 13 wceq wff A ∘ B = x y | ∃ z x B z ∧ z A y