setcco

Description: Composition in the category of sets. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	setcbas.c	⊢ 𝐶 = ( SetCat ‘ 𝑈 )
	setcbas.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	setcco.o	⊢ · = ( comp ‘ 𝐶 )
	setcco.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
	setcco.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
	setcco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
	setcco.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
	setcco.g	⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑍 )
Assertion	setcco	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		setcbas.c	⊢ 𝐶 = ( SetCat ‘ 𝑈 )
2		setcbas.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		setcco.o	⊢ · = ( comp ‘ 𝐶 )
4		setcco.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
5		setcco.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
6		setcco.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
7		setcco.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
8		setcco.g	⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑍 )
9	1 2 3	setccofval	⊢ ( 𝜑 → · = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧 ∈ 𝑈 ↦ ( 𝑔 ∈ ( 𝑧 ↑_m ( 2^nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2^nd ‘ 𝑣 ) ↑_m ( 1^st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑧 = 𝑍 )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2^nd ‘ 𝑣 ) = ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
13		op2ndg	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
14	4 5 13	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
16	12 15	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 2^nd ‘ 𝑣 ) = 𝑌 )
17	10 16	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑧 ↑_m ( 2^nd ‘ 𝑣 ) ) = ( 𝑍 ↑_m 𝑌 ) )
18	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1^st ‘ 𝑣 ) = ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
19		op1stg	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
20	4 5 19	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
21	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
22	18 21	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 1^st ‘ 𝑣 ) = 𝑋 )
23	16 22	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( ( 2^nd ‘ 𝑣 ) ↑_m ( 1^st ‘ 𝑣 ) ) = ( 𝑌 ↑_m 𝑋 ) )
24		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∘ 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
25	17 23 24	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑣 = ⟨ 𝑋 , 𝑌 ⟩ ∧ 𝑧 = 𝑍 ) ) → ( 𝑔 ∈ ( 𝑧 ↑_m ( 2^nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2^nd ‘ 𝑣 ) ↑_m ( 1^st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( 𝑍 ↑_m 𝑌 ) , 𝑓 ∈ ( 𝑌 ↑_m 𝑋 ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
26	4 5	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑈 × 𝑈 ) )
27		ovex	⊢ ( 𝑍 ↑_m 𝑌 ) ∈ V
28		ovex	⊢ ( 𝑌 ↑_m 𝑋 ) ∈ V
29	27 28	mpoex	⊢ ( 𝑔 ∈ ( 𝑍 ↑_m 𝑌 ) , 𝑓 ∈ ( 𝑌 ↑_m 𝑋 ) ↦ ( 𝑔 ∘ 𝑓 ) ) ∈ V
30	29	a1i	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑍 ↑_m 𝑌 ) , 𝑓 ∈ ( 𝑌 ↑_m 𝑋 ) ↦ ( 𝑔 ∘ 𝑓 ) ) ∈ V )
31	9 25 26 6 30	ovmpod	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) = ( 𝑔 ∈ ( 𝑍 ↑_m 𝑌 ) , 𝑓 ∈ ( 𝑌 ↑_m 𝑋 ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
32		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑔 = 𝐺 )
33		simprr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
34	32 33	coeq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝑔 ∘ 𝑓 ) = ( 𝐺 ∘ 𝐹 ) )
35	6 5	elmapd	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑍 ↑_m 𝑌 ) ↔ 𝐺 : 𝑌 ⟶ 𝑍 ) )
36	8 35	mpbird	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 ↑_m 𝑌 ) )
37	5 4	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑌 ↑_m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
38	7 37	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑌 ↑_m 𝑋 ) )
39		coexg	⊢ ( ( 𝐺 ∈ ( 𝑍 ↑_m 𝑌 ) ∧ 𝐹 ∈ ( 𝑌 ↑_m 𝑋 ) ) → ( 𝐺 ∘ 𝐹 ) ∈ V )
40	36 38 39	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ V )
41	31 34 36 38 40	ovmpod	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )

Metamath Proof Explorer

Theorem setcco

Proof