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	⊢ ( 𝐴 ∘ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	ccom	⊢ ( 𝐴 ∘ 𝐵 )
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5		vz	⊢ 𝑧
6	3	cv	⊢ 𝑥
7	5	cv	⊢ 𝑧
8	6 7 1	wbr	⊢ 𝑥 𝐵 𝑧
9	4	cv	⊢ 𝑦
10	7 9 0	wbr	⊢ 𝑧 𝐴 𝑦
11	8 10	wa	⊢ ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 )
12	11 5	wex	⊢ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 )
13	12 3 4	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) }
14	2 13	wceq	⊢ ( 𝐴 ∘ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) }

Metamath Proof Explorer

Definition df-co

Detailed syntax breakdown