yonedalem3

	Ref	Expression
Hypotheses	yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
	yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
	yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
	yoneda.h	⊢ 𝐻 = ( Hom_F ‘ 𝑄 )
	yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×_c 𝑂 ) FuncCat 𝑇 )
	yoneda.e	⊢ 𝐸 = ( 𝑂 eval_F 𝑆 )
	yoneda.z	⊢ 𝑍 = ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) )
	yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
	yoneda.u	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
	yoneda.v	⊢ ( 𝜑 → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
	yoneda.m	⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) )
Assertion	yonedalem3	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 ) 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
4		yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
5		yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
6		yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
7		yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
8		yoneda.h	⊢ 𝐻 = ( Hom_F ‘ 𝑄 )
9		yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×_c 𝑂 ) FuncCat 𝑇 )
10		yoneda.e	⊢ 𝐸 = ( 𝑂 eval_F 𝑆 )
11		yoneda.z	⊢ 𝑍 = ( 𝐻 ∘_func ( ( ⟨ ( 1^st ‘ 𝑌 ) , tpos ( 2^nd ‘ 𝑌 ) ⟩ ∘_func ( 𝑄 2^nd_F 𝑂 ) ) ⟨,⟩_F ( 𝑄 1^st_F 𝑂 ) ) )
12		yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13		yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
14		yoneda.u	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
15		yoneda.v	⊢ ( 𝜑 → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
16		yoneda.m	⊢ 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) )
17		ovex	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ∈ V
18	17	mptex	⊢ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) ∈ V
19	16 18	fnmpoi	⊢ 𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 )
20	19	a1i	⊢ ( 𝜑 → 𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
21	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ Cat )
22	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑉 ∈ 𝑊 )
23	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
24	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
25		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑔 ∈ ( 𝑂 Func 𝑆 ) )
26		simprr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
27	1 2 3 4 5 6 7 8 9 10 11 21 22 23 24 25 26 16	yonedalem3a	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑔 𝑀 𝑦 ) = ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ( 𝑂 Nat 𝑆 ) 𝑔 ) ↦ ( ( 𝑎 ‘ 𝑦 ) ‘ ( 1 ‘ 𝑦 ) ) ) ∧ ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ) )
28	27	simprd	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) )
29		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
30		eqid	⊢ ( 𝑄 ×_c 𝑂 ) = ( 𝑄 ×_c 𝑂 )
31	7	fucbas	⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 )
32	4 2	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
33	30 31 32	xpcbas	⊢ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) = ( Base ‘ ( 𝑄 ×_c 𝑂 ) )
34		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
35		relfunc	⊢ Rel ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 )
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	⊢ ( 𝜑 → ( 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ) )
37	36	simpld	⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) )
38		1st2ndbr	⊢ ( ( Rel ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ∧ 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ) → ( 1^st ‘ 𝑍 ) ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ( 2^nd ‘ 𝑍 ) )
39	35 37 38	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑍 ) ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ( 2^nd ‘ 𝑍 ) )
40	33 34 39	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑍 ) : ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ⟶ ( Base ‘ 𝑇 ) )
41	40	fovcdmda	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ∈ ( Base ‘ 𝑇 ) )
42	6 22	setcbas	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → 𝑉 = ( Base ‘ 𝑇 ) )
43	41 42	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ∈ 𝑉 )
44	36	simprd	⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) )
45		1st2ndbr	⊢ ( ( Rel ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ) → ( 1^st ‘ 𝐸 ) ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ( 2^nd ‘ 𝐸 ) )
46	35 44 45	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐸 ) ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ( 2^nd ‘ 𝐸 ) )
47	33 34 46	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐸 ) : ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ⟶ ( Base ‘ 𝑇 ) )
48	47	fovcdmda	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ∈ ( Base ‘ 𝑇 ) )
49	48 42	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ∈ 𝑉 )
50	6 22 29 43 49	elsetchom	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ) ↔ ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ) )
51	28 50	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ) )
52	51	ralrimivva	⊢ ( 𝜑 → ∀ 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∀ 𝑦 ∈ 𝐵 ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ) )
53		fveq2	⊢ ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ ⟨ 𝑔 , 𝑦 ⟩ ) )
54		df-ov	⊢ ( 𝑔 𝑀 𝑦 ) = ( 𝑀 ‘ ⟨ 𝑔 , 𝑦 ⟩ )
55	53 54	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( 𝑀 ‘ 𝑧 ) = ( 𝑔 𝑀 𝑦 ) )
56		fveq2	⊢ ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝑔 , 𝑦 ⟩ ) )
57		df-ov	⊢ ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ 𝑔 , 𝑦 ⟩ )
58	56 57	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) = ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) )
59		fveq2	⊢ ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝑔 , 𝑦 ⟩ ) )
60		df-ov	⊢ ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ 𝑔 , 𝑦 ⟩ )
61	59 60	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) = ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) )
62	58 61	oveq12d	⊢ ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) = ( ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ) )
63	55 62	eleq12d	⊢ ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 𝑀 ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) ↔ ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ) ) )
64	63	ralxp	⊢ ( ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀 ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) ↔ ∀ 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∀ 𝑦 ∈ 𝐵 ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1^st ‘ 𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1^st ‘ 𝐸 ) 𝑦 ) ) )
65	52 64	sylibr	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀 ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) )
66		ovex	⊢ ( 𝑂 Func 𝑆 ) ∈ V
67	2	fvexi	⊢ 𝐵 ∈ V
68	66 67	mpoex	⊢ ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑎 ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎 ‘ 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) ) ) ∈ V
69	16 68	eqeltri	⊢ 𝑀 ∈ V
70	69	elixp	⊢ ( 𝑀 ∈ X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) ↔ ( 𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀 ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) ) )
71	20 65 70	sylanbrc	⊢ ( 𝜑 → 𝑀 ∈ X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) )
72	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝐶 ∈ Cat )
73	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝑉 ∈ 𝑊 )
74	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
75	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
76		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
77		xp1st	⊢ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 1^st ‘ 𝑧 ) ∈ ( 𝑂 Func 𝑆 ) )
78	76 77	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 1^st ‘ 𝑧 ) ∈ ( 𝑂 Func 𝑆 ) )
79		xp2nd	⊢ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 2^nd ‘ 𝑧 ) ∈ 𝐵 )
80	76 79	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 2^nd ‘ 𝑧 ) ∈ 𝐵 )
81		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
82		xp1st	⊢ ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 1^st ‘ 𝑤 ) ∈ ( 𝑂 Func 𝑆 ) )
83	81 82	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 1^st ‘ 𝑤 ) ∈ ( 𝑂 Func 𝑆 ) )
84		xp2nd	⊢ ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 2^nd ‘ 𝑤 ) ∈ 𝐵 )
85	81 84	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 2^nd ‘ 𝑤 ) ∈ 𝐵 )
86		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) )
87		eqid	⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
88	7 87	fuchom	⊢ ( 𝑂 Nat 𝑆 ) = ( Hom ‘ 𝑄 )
89		eqid	⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
90		eqid	⊢ ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) = ( Hom ‘ ( 𝑄 ×_c 𝑂 ) )
91	30 33 88 89 90 76 81	xpchom	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) = ( ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) × ( ( 2^nd ‘ 𝑧 ) ( Hom ‘ 𝑂 ) ( 2^nd ‘ 𝑤 ) ) ) )
92		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
93	92 4	oppchom	⊢ ( ( 2^nd ‘ 𝑧 ) ( Hom ‘ 𝑂 ) ( 2^nd ‘ 𝑤 ) ) = ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) )
94	93	xpeq2i	⊢ ( ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) × ( ( 2^nd ‘ 𝑧 ) ( Hom ‘ 𝑂 ) ( 2^nd ‘ 𝑤 ) ) ) = ( ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) × ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) )
95	91 94	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) = ( ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) × ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) )
96	86 95	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 ∈ ( ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) × ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) )
97		xp1st	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) × ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) → ( 1^st ‘ 𝑔 ) ∈ ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) )
98	96 97	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 1^st ‘ 𝑔 ) ∈ ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) )
99		xp2nd	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) × ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) → ( 2^nd ‘ 𝑔 ) ∈ ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) )
100	96 99	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 2^nd ‘ 𝑔 ) ∈ ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) )
101	1 2 3 4 5 6 7 8 9 10 11 72 73 74 75 78 80 83 85 98 100 16	yonedalem3b	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( ( 1^st ‘ 𝑤 ) 𝑀 ( 2^nd ‘ 𝑤 ) ) ( ⟨ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) , ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑤 ) ) ) ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝑍 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ( 2^nd ‘ 𝑔 ) ) ) = ( ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ( 2^nd ‘ 𝑔 ) ) ( ⟨ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) , ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑧 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑤 ) ) ) ( ( 1^st ‘ 𝑧 ) 𝑀 ( 2^nd ‘ 𝑧 ) ) ) )
102		1st2nd2	⊢ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
103	76 102	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
104	103	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
105		df-ov	⊢ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
106	104 105	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) )
107		1st2nd2	⊢ ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
108	81 107	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
109	108	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝑍 ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
110		df-ov	⊢ ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑤 ) ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
111	109 110	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝑍 ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑤 ) ) )
112	106 111	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑍 ) ‘ 𝑤 ) ⟩ = ⟨ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) , ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑤 ) ) ⟩ )
113	108	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
114		df-ov	⊢ ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑤 ) ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
115	113 114	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑤 ) ) )
116	112 115	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) , ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑤 ) ) ) )
117	108	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀 ‘ 𝑤 ) = ( 𝑀 ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
118		df-ov	⊢ ( ( 1^st ‘ 𝑤 ) 𝑀 ( 2^nd ‘ 𝑤 ) ) = ( 𝑀 ‘ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
119	117 118	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀 ‘ 𝑤 ) = ( ( 1^st ‘ 𝑤 ) 𝑀 ( 2^nd ‘ 𝑤 ) ) )
120	103 108	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( 2^nd ‘ 𝑍 ) 𝑤 ) = ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝑍 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
121		1st2nd2	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1^st ‘ 𝑤 ) ) × ( ( 2^nd ‘ 𝑤 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑧 ) ) ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
122	96 121	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
123	120 122	fveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) = ( ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝑍 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ) )
124		df-ov	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝑍 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ( 2^nd ‘ 𝑔 ) ) = ( ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝑍 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
125	123 124	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) = ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝑍 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ( 2^nd ‘ 𝑔 ) ) )
126	116 119 125	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑀 ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 1^st ‘ 𝑤 ) 𝑀 ( 2^nd ‘ 𝑤 ) ) ( ⟨ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) , ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑤 ) ) ) ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝑍 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ( 2^nd ‘ 𝑔 ) ) ) )
127	103	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
128		df-ov	⊢ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
129	127 128	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑧 ) ) )
130	106 129	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ⟩ = ⟨ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) , ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑧 ) ) ⟩ )
131	130 115	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) , ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑧 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑤 ) ) ) )
132	103 108	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( 2^nd ‘ 𝐸 ) 𝑤 ) = ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
133	132 122	fveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) = ( ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ) )
134		df-ov	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ( 2^nd ‘ 𝑔 ) ) = ( ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ‘ ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
135	133 134	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) = ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ( 2^nd ‘ 𝑔 ) ) )
136	103	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ) )
137		df-ov	⊢ ( ( 1^st ‘ 𝑧 ) 𝑀 ( 2^nd ‘ 𝑧 ) ) = ( 𝑀 ‘ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
138	136 137	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀 ‘ 𝑧 ) = ( ( 1^st ‘ 𝑧 ) 𝑀 ( 2^nd ‘ 𝑧 ) ) )
139	131 135 138	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2^nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) ( 𝑀 ‘ 𝑧 ) ) = ( ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ( 2^nd ‘ 𝐸 ) ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ( 2^nd ‘ 𝑔 ) ) ( ⟨ ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝑍 ) ( 2^nd ‘ 𝑧 ) ) , ( ( 1^st ‘ 𝑧 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑧 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) ( 2^nd ‘ 𝑤 ) ) ) ( ( 1^st ‘ 𝑧 ) 𝑀 ( 2^nd ‘ 𝑧 ) ) ) )
140	101 126 139	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑀 ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) ( 𝑀 ‘ 𝑧 ) ) )
141	140	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ( ( 𝑀 ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) ( 𝑀 ‘ 𝑧 ) ) )
142		eqid	⊢ ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 ) = ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 )
143		eqid	⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
144	142 33 90 29 143 37 44	isnat2	⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑍 ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 ) 𝐸 ) ↔ ( 𝑀 ∈ X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ) ∧ ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×_c 𝑂 ) ) 𝑤 ) ( ( 𝑀 ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ 𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐸 ) 𝑤 ) ‘ 𝑔 ) ( ⟨ ( ( 1^st ‘ 𝑍 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1^st ‘ 𝐸 ) ‘ 𝑤 ) ) ( 𝑀 ‘ 𝑧 ) ) ) ) )
145	71 141 144	mpbir2and	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 ) 𝐸 ) )

Metamath Proof Explorer

Theorem yonedalem3

Proof