MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  yonedalem3b Structured version   Visualization version   GIF version

Theorem yonedalem3b 18228
Description: Lemma for yoneda 18232. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
yoneda.y π‘Œ = (Yonβ€˜πΆ)
yoneda.b 𝐡 = (Baseβ€˜πΆ)
yoneda.1 1 = (Idβ€˜πΆ)
yoneda.o 𝑂 = (oppCatβ€˜πΆ)
yoneda.s 𝑆 = (SetCatβ€˜π‘ˆ)
yoneda.t 𝑇 = (SetCatβ€˜π‘‰)
yoneda.q 𝑄 = (𝑂 FuncCat 𝑆)
yoneda.h 𝐻 = (HomFβ€˜π‘„)
yoneda.r 𝑅 = ((𝑄 Γ—c 𝑂) FuncCat 𝑇)
yoneda.e 𝐸 = (𝑂 evalF 𝑆)
yoneda.z 𝑍 = (𝐻 ∘func ((⟨(1st β€˜π‘Œ), tpos (2nd β€˜π‘Œ)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
yoneda.c (πœ‘ β†’ 𝐢 ∈ Cat)
yoneda.w (πœ‘ β†’ 𝑉 ∈ π‘Š)
yoneda.u (πœ‘ β†’ ran (Homf β€˜πΆ) βŠ† π‘ˆ)
yoneda.v (πœ‘ β†’ (ran (Homf β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
yonedalem21.f (πœ‘ β†’ 𝐹 ∈ (𝑂 Func 𝑆))
yonedalem21.x (πœ‘ β†’ 𝑋 ∈ 𝐡)
yonedalem22.g (πœ‘ β†’ 𝐺 ∈ (𝑂 Func 𝑆))
yonedalem22.p (πœ‘ β†’ 𝑃 ∈ 𝐡)
yonedalem22.a (πœ‘ β†’ 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
yonedalem22.k (πœ‘ β†’ 𝐾 ∈ (𝑃(Hom β€˜πΆ)𝑋))
yonedalem3.m 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), π‘₯ ∈ 𝐡 ↦ (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘₯)(𝑂 Nat 𝑆)𝑓) ↦ ((π‘Žβ€˜π‘₯)β€˜( 1 β€˜π‘₯))))
Assertion
Ref Expression
yonedalem3b (πœ‘ β†’ ((𝐺𝑀𝑃)(⟨(𝐹(1st β€˜π‘)𝑋), (𝐺(1st β€˜π‘)𝑃)⟩(compβ€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃))(𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾)) = ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾)(⟨(𝐹(1st β€˜π‘)𝑋), (𝐹(1st β€˜πΈ)𝑋)⟩(compβ€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃))(𝐹𝑀𝑋)))
Distinct variable groups:   𝑓,π‘Ž,π‘₯, 1   𝐴,π‘Ž   𝐢,π‘Ž,𝑓,π‘₯   𝐸,π‘Ž,𝑓   𝐹,π‘Ž,𝑓,π‘₯   𝐾,π‘Ž   𝐡,π‘Ž,𝑓,π‘₯   𝐺,π‘Ž,𝑓,π‘₯   𝑂,π‘Ž,𝑓,π‘₯   𝑆,π‘Ž,𝑓,π‘₯   𝑄,π‘Ž,𝑓,π‘₯   𝑇,𝑓   𝑃,π‘Ž,𝑓,π‘₯   πœ‘,π‘Ž,𝑓,π‘₯   π‘Œ,π‘Ž,𝑓,π‘₯   𝑍,π‘Ž,𝑓,π‘₯   𝑋,π‘Ž,𝑓,π‘₯
Allowed substitution hints:   𝐴(π‘₯,𝑓)   𝑅(π‘₯,𝑓,π‘Ž)   𝑇(π‘₯,π‘Ž)   π‘ˆ(π‘₯,𝑓,π‘Ž)   𝐸(π‘₯)   𝐻(π‘₯,𝑓,π‘Ž)   𝐾(π‘₯,𝑓)   𝑀(π‘₯,𝑓,π‘Ž)   𝑉(π‘₯,𝑓,π‘Ž)   π‘Š(π‘₯,𝑓,π‘Ž)

Proof of Theorem yonedalem3b
Dummy variables 𝑏 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7413 . . . . . . . 8 (𝑏 = π‘Ž β†’ (𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏) = (𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž))
21oveq1d 7420 . . . . . . 7 (𝑏 = π‘Ž β†’ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)) = ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)))
32fveq1d 6890 . . . . . 6 (𝑏 = π‘Ž β†’ (((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ) = (((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ))
43fveq1d 6890 . . . . 5 (𝑏 = π‘Ž β†’ ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)) = ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)))
54cbvmptv 5260 . . . 4 (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)))
6 yoneda.q . . . . . . . . 9 𝑄 = (𝑂 FuncCat 𝑆)
7 eqid 2732 . . . . . . . . 9 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
8 yoneda.o . . . . . . . . . 10 𝑂 = (oppCatβ€˜πΆ)
9 yoneda.b . . . . . . . . . 10 𝐡 = (Baseβ€˜πΆ)
108, 9oppcbas 17659 . . . . . . . . 9 𝐡 = (Baseβ€˜π‘‚)
11 eqid 2732 . . . . . . . . 9 (compβ€˜π‘†) = (compβ€˜π‘†)
12 eqid 2732 . . . . . . . . 9 (compβ€˜π‘„) = (compβ€˜π‘„)
13 eqid 2732 . . . . . . . . . . . 12 (Hom β€˜πΆ) = (Hom β€˜πΆ)
146, 7fuchom 17909 . . . . . . . . . . . 12 (𝑂 Nat 𝑆) = (Hom β€˜π‘„)
15 relfunc 17808 . . . . . . . . . . . . 13 Rel (𝐢 Func 𝑄)
16 yoneda.y . . . . . . . . . . . . . 14 π‘Œ = (Yonβ€˜πΆ)
17 yoneda.c . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐢 ∈ Cat)
18 yoneda.s . . . . . . . . . . . . . 14 𝑆 = (SetCatβ€˜π‘ˆ)
19 yoneda.w . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑉 ∈ π‘Š)
20 yoneda.v . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (ran (Homf β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
2120unssbd 4187 . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘ˆ βŠ† 𝑉)
2219, 21ssexd 5323 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘ˆ ∈ V)
23 yoneda.u . . . . . . . . . . . . . 14 (πœ‘ β†’ ran (Homf β€˜πΆ) βŠ† π‘ˆ)
2416, 17, 8, 18, 6, 22, 23yoncl 18211 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ∈ (𝐢 Func 𝑄))
25 1st2ndbr 8024 . . . . . . . . . . . . 13 ((Rel (𝐢 Func 𝑄) ∧ π‘Œ ∈ (𝐢 Func 𝑄)) β†’ (1st β€˜π‘Œ)(𝐢 Func 𝑄)(2nd β€˜π‘Œ))
2615, 24, 25sylancr 587 . . . . . . . . . . . 12 (πœ‘ β†’ (1st β€˜π‘Œ)(𝐢 Func 𝑄)(2nd β€˜π‘Œ))
27 yonedalem22.p . . . . . . . . . . . 12 (πœ‘ β†’ 𝑃 ∈ 𝐡)
28 yonedalem21.x . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 ∈ 𝐡)
299, 13, 14, 26, 27, 28funcf2 17814 . . . . . . . . . . 11 (πœ‘ β†’ (𝑃(2nd β€˜π‘Œ)𝑋):(𝑃(Hom β€˜πΆ)𝑋)⟢(((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)((1st β€˜π‘Œ)β€˜π‘‹)))
30 yonedalem22.k . . . . . . . . . . 11 (πœ‘ β†’ 𝐾 ∈ (𝑃(Hom β€˜πΆ)𝑋))
3129, 30ffvelcdmd 7084 . . . . . . . . . 10 (πœ‘ β†’ ((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ) ∈ (((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)((1st β€˜π‘Œ)β€˜π‘‹)))
3231adantr 481 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ) ∈ (((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)((1st β€˜π‘Œ)β€˜π‘‹)))
33 simpr 485 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹))
34 yonedalem22.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
3534adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
366, 7, 12, 33, 35fuccocl 17913 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž) ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐺))
3727adantr 481 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ 𝑃 ∈ 𝐡)
386, 7, 10, 11, 12, 32, 36, 37fuccoval 17912 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ) = (((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)β€˜π‘ƒ)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ), ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ))(((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)))
396, 7, 10, 11, 12, 33, 35, 37fuccoval 17912 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)β€˜π‘ƒ) = ((π΄β€˜π‘ƒ)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ), ((1st β€˜πΉ)β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ))(π‘Žβ€˜π‘ƒ)))
4022adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ π‘ˆ ∈ V)
41 eqid 2732 . . . . . . . . . . . . . . 15 (Baseβ€˜π‘†) = (Baseβ€˜π‘†)
42 relfunc 17808 . . . . . . . . . . . . . . . 16 Rel (𝑂 Func 𝑆)
436fucbas 17908 . . . . . . . . . . . . . . . . . 18 (𝑂 Func 𝑆) = (Baseβ€˜π‘„)
449, 43, 26funcf1 17812 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (1st β€˜π‘Œ):𝐡⟢(𝑂 Func 𝑆))
4544, 28ffvelcdmd 7084 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((1st β€˜π‘Œ)β€˜π‘‹) ∈ (𝑂 Func 𝑆))
46 1st2ndbr 8024 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ ((1st β€˜π‘Œ)β€˜π‘‹) ∈ (𝑂 Func 𝑆)) β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))(𝑂 Func 𝑆)(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹)))
4742, 45, 46sylancr 587 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))(𝑂 Func 𝑆)(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹)))
4810, 41, 47funcf1 17812 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘‹)):𝐡⟢(Baseβ€˜π‘†))
4918, 22setcbas 18024 . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘ˆ = (Baseβ€˜π‘†))
5049feq3d 6701 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹)):π΅βŸΆπ‘ˆ ↔ (1st β€˜((1st β€˜π‘Œ)β€˜π‘‹)):𝐡⟢(Baseβ€˜π‘†)))
5148, 50mpbird 256 . . . . . . . . . . . . 13 (πœ‘ β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘‹)):π΅βŸΆπ‘ˆ)
5251, 27ffvelcdmd 7084 . . . . . . . . . . . 12 (πœ‘ β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ) ∈ π‘ˆ)
5352adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ) ∈ π‘ˆ)
54 yonedalem21.f . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹 ∈ (𝑂 Func 𝑆))
55 1st2ndbr 8024 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) β†’ (1st β€˜πΉ)(𝑂 Func 𝑆)(2nd β€˜πΉ))
5642, 54, 55sylancr 587 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1st β€˜πΉ)(𝑂 Func 𝑆)(2nd β€˜πΉ))
5710, 41, 56funcf1 17812 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1st β€˜πΉ):𝐡⟢(Baseβ€˜π‘†))
5849feq3d 6701 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1st β€˜πΉ):π΅βŸΆπ‘ˆ ↔ (1st β€˜πΉ):𝐡⟢(Baseβ€˜π‘†)))
5957, 58mpbird 256 . . . . . . . . . . . . 13 (πœ‘ β†’ (1st β€˜πΉ):π΅βŸΆπ‘ˆ)
6059, 27ffvelcdmd 7084 . . . . . . . . . . . 12 (πœ‘ β†’ ((1st β€˜πΉ)β€˜π‘ƒ) ∈ π‘ˆ)
6160adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((1st β€˜πΉ)β€˜π‘ƒ) ∈ π‘ˆ)
62 yonedalem22.g . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐺 ∈ (𝑂 Func 𝑆))
63 1st2ndbr 8024 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ 𝐺 ∈ (𝑂 Func 𝑆)) β†’ (1st β€˜πΊ)(𝑂 Func 𝑆)(2nd β€˜πΊ))
6442, 62, 63sylancr 587 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1st β€˜πΊ)(𝑂 Func 𝑆)(2nd β€˜πΊ))
6510, 41, 64funcf1 17812 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1st β€˜πΊ):𝐡⟢(Baseβ€˜π‘†))
6665, 27ffvelcdmd 7084 . . . . . . . . . . . . 13 (πœ‘ β†’ ((1st β€˜πΊ)β€˜π‘ƒ) ∈ (Baseβ€˜π‘†))
6766, 49eleqtrrd 2836 . . . . . . . . . . . 12 (πœ‘ β†’ ((1st β€˜πΊ)β€˜π‘ƒ) ∈ π‘ˆ)
6867adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((1st β€˜πΊ)β€˜π‘ƒ) ∈ π‘ˆ)
697, 33nat1st2nd 17898 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ π‘Ž ∈ (⟨(1st β€˜((1st β€˜π‘Œ)β€˜π‘‹)), (2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))⟩(𝑂 Nat 𝑆)⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩))
70 eqid 2732 . . . . . . . . . . . . 13 (Hom β€˜π‘†) = (Hom β€˜π‘†)
717, 69, 10, 70, 37natcl 17900 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (π‘Žβ€˜π‘ƒ) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)(Hom β€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ)))
7218, 40, 70, 53, 61elsetchom 18027 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π‘Žβ€˜π‘ƒ) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)(Hom β€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ)) ↔ (π‘Žβ€˜π‘ƒ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟢((1st β€˜πΉ)β€˜π‘ƒ)))
7371, 72mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (π‘Žβ€˜π‘ƒ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟢((1st β€˜πΉ)β€˜π‘ƒ))
747, 34nat1st2nd 17898 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 ∈ (⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩(𝑂 Nat 𝑆)⟨(1st β€˜πΊ), (2nd β€˜πΊ)⟩))
757, 74, 10, 70, 27natcl 17900 . . . . . . . . . . . . 13 (πœ‘ β†’ (π΄β€˜π‘ƒ) ∈ (((1st β€˜πΉ)β€˜π‘ƒ)(Hom β€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ)))
7618, 22, 70, 60, 67elsetchom 18027 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΄β€˜π‘ƒ) ∈ (((1st β€˜πΉ)β€˜π‘ƒ)(Hom β€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ)) ↔ (π΄β€˜π‘ƒ):((1st β€˜πΉ)β€˜π‘ƒ)⟢((1st β€˜πΊ)β€˜π‘ƒ)))
7775, 76mpbid 231 . . . . . . . . . . . 12 (πœ‘ β†’ (π΄β€˜π‘ƒ):((1st β€˜πΉ)β€˜π‘ƒ)⟢((1st β€˜πΊ)β€˜π‘ƒ))
7877adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (π΄β€˜π‘ƒ):((1st β€˜πΉ)β€˜π‘ƒ)⟢((1st β€˜πΊ)β€˜π‘ƒ))
7918, 40, 11, 53, 61, 68, 73, 78setcco 18029 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π΄β€˜π‘ƒ)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ), ((1st β€˜πΉ)β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ))(π‘Žβ€˜π‘ƒ)) = ((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)))
8039, 79eqtrd 2772 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)β€˜π‘ƒ) = ((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)))
8180oveq1d 7420 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)β€˜π‘ƒ)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ), ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ))(((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)) = (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ))(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ), ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ))(((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)))
8244, 27ffvelcdmd 7084 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1st β€˜π‘Œ)β€˜π‘ƒ) ∈ (𝑂 Func 𝑆))
83 1st2ndbr 8024 . . . . . . . . . . . . . 14 ((Rel (𝑂 Func 𝑆) ∧ ((1st β€˜π‘Œ)β€˜π‘ƒ) ∈ (𝑂 Func 𝑆)) β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))(𝑂 Func 𝑆)(2nd β€˜((1st β€˜π‘Œ)β€˜π‘ƒ)))
8442, 82, 83sylancr 587 . . . . . . . . . . . . 13 (πœ‘ β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))(𝑂 Func 𝑆)(2nd β€˜((1st β€˜π‘Œ)β€˜π‘ƒ)))
8510, 41, 84funcf1 17812 . . . . . . . . . . . 12 (πœ‘ β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ)):𝐡⟢(Baseβ€˜π‘†))
8685, 27ffvelcdmd 7084 . . . . . . . . . . 11 (πœ‘ β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ) ∈ (Baseβ€˜π‘†))
8786, 49eleqtrrd 2836 . . . . . . . . . 10 (πœ‘ β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ) ∈ π‘ˆ)
8887adantr 481 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ) ∈ π‘ˆ)
897, 31nat1st2nd 17898 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ) ∈ (⟨(1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ)), (2nd β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))⟩(𝑂 Nat 𝑆)⟨(1st β€˜((1st β€˜π‘Œ)β€˜π‘‹)), (2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))⟩))
907, 89, 10, 70, 27natcl 17900 . . . . . . . . . . 11 (πœ‘ β†’ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ)(Hom β€˜π‘†)((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)))
9118, 22, 70, 87, 52elsetchom 18027 . . . . . . . . . . 11 (πœ‘ β†’ ((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ)(Hom β€˜π‘†)((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)) ↔ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)))
9290, 91mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ))
9392adantr 481 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ))
94 fco 6738 . . . . . . . . . 10 (((π΄β€˜π‘ƒ):((1st β€˜πΉ)β€˜π‘ƒ)⟢((1st β€˜πΊ)β€˜π‘ƒ) ∧ (π‘Žβ€˜π‘ƒ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟢((1st β€˜πΉ)β€˜π‘ƒ)) β†’ ((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟢((1st β€˜πΊ)β€˜π‘ƒ))
9578, 73, 94syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟢((1st β€˜πΊ)β€˜π‘ƒ))
9618, 40, 11, 88, 53, 68, 93, 95setcco 18029 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ))(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ), ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ))(((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)) = (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)) ∘ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)))
9738, 81, 963eqtrd 2776 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ) = (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)) ∘ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)))
9897fveq1d 6890 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)) = ((((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)) ∘ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ))β€˜( 1 β€˜π‘ƒ)))
99 yoneda.1 . . . . . . . . . 10 1 = (Idβ€˜πΆ)
1009, 13, 99, 17, 27catidcl 17622 . . . . . . . . 9 (πœ‘ β†’ ( 1 β€˜π‘ƒ) ∈ (𝑃(Hom β€˜πΆ)𝑃))
10116, 9, 17, 27, 13, 27yon11 18213 . . . . . . . . 9 (πœ‘ β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ) = (𝑃(Hom β€˜πΆ)𝑃))
102100, 101eleqtrrd 2836 . . . . . . . 8 (πœ‘ β†’ ( 1 β€˜π‘ƒ) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ))
103102adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ( 1 β€˜π‘ƒ) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ))
104 fvco3 6987 . . . . . . 7 (((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ) ∧ ( 1 β€˜π‘ƒ) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘ƒ))β€˜π‘ƒ)) β†’ ((((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)) ∘ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ))β€˜( 1 β€˜π‘ƒ)) = (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ))β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))))
10593, 103, 104syl2anc 584 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ)) ∘ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ))β€˜( 1 β€˜π‘ƒ)) = (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ))β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))))
10693, 103ffvelcdmd 7084 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ))
107 fvco3 6987 . . . . . . . 8 (((π‘Žβ€˜π‘ƒ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟢((1st β€˜πΉ)β€˜π‘ƒ) ∧ ((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)) β†’ (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ))β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) = ((π΄β€˜π‘ƒ)β€˜((π‘Žβ€˜π‘ƒ)β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)))))
10873, 106, 107syl2anc 584 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ))β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) = ((π΄β€˜π‘ƒ)β€˜((π‘Žβ€˜π‘ƒ)β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)))))
10917adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ 𝐢 ∈ Cat)
11028adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ 𝑋 ∈ 𝐡)
111 eqid 2732 . . . . . . . . . . . 12 (compβ€˜πΆ) = (compβ€˜πΆ)
11230adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ 𝐾 ∈ (𝑃(Hom β€˜πΆ)𝑋))
113100adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ( 1 β€˜π‘ƒ) ∈ (𝑃(Hom β€˜πΆ)𝑃))
11416, 9, 109, 37, 13, 110, 111, 37, 112, 113yon2 18215 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)) = (𝐾(βŸ¨π‘ƒ, π‘ƒβŸ©(compβ€˜πΆ)𝑋)( 1 β€˜π‘ƒ)))
1159, 13, 99, 109, 37, 111, 110, 112catrid 17624 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (𝐾(βŸ¨π‘ƒ, π‘ƒβŸ©(compβ€˜πΆ)𝑋)( 1 β€˜π‘ƒ)) = 𝐾)
116114, 115eqtrd 2772 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)) = 𝐾)
117116fveq2d 6892 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π‘Žβ€˜π‘ƒ)β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) = ((π‘Žβ€˜π‘ƒ)β€˜πΎ))
118 eqid 2732 . . . . . . . . . . . . . . 15 (Hom β€˜π‘‚) = (Hom β€˜π‘‚)
11910, 118, 70, 47, 28, 27funcf2 17814 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃):(𝑋(Hom β€˜π‘‚)𝑃)⟢(((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)(Hom β€˜π‘†)((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)))
12013, 8oppchom 17656 . . . . . . . . . . . . . . 15 (𝑋(Hom β€˜π‘‚)𝑃) = (𝑃(Hom β€˜πΆ)𝑋)
12130, 120eleqtrrdi 2844 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐾 ∈ (𝑋(Hom β€˜π‘‚)𝑃))
122119, 121ffvelcdmd 7084 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)(Hom β€˜π‘†)((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)))
12351, 28ffvelcdmd 7084 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹) ∈ π‘ˆ)
12418, 22, 70, 123, 52elsetchom 18027 . . . . . . . . . . . . 13 (πœ‘ β†’ (((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)(Hom β€˜π‘†)((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)) ↔ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)))
125122, 124mpbid 231 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ))
126125adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ))
1279, 13, 99, 17, 28catidcl 17622 . . . . . . . . . . . . 13 (πœ‘ β†’ ( 1 β€˜π‘‹) ∈ (𝑋(Hom β€˜πΆ)𝑋))
12816, 9, 17, 28, 13, 28yon11 18213 . . . . . . . . . . . . 13 (πœ‘ β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹) = (𝑋(Hom β€˜πΆ)𝑋))
129127, 128eleqtrrd 2836 . . . . . . . . . . . 12 (πœ‘ β†’ ( 1 β€˜π‘‹) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹))
130129adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ( 1 β€˜π‘‹) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹))
131 fvco3 6987 . . . . . . . . . . 11 ((((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ) ∧ ( 1 β€˜π‘‹) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)) β†’ (((π‘Žβ€˜π‘ƒ) ∘ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ))β€˜( 1 β€˜π‘‹)) = ((π‘Žβ€˜π‘ƒ)β€˜(((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)β€˜( 1 β€˜π‘‹))))
132126, 130, 131syl2anc 584 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((π‘Žβ€˜π‘ƒ) ∘ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ))β€˜( 1 β€˜π‘‹)) = ((π‘Žβ€˜π‘ƒ)β€˜(((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)β€˜( 1 β€˜π‘‹))))
133121adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ 𝐾 ∈ (𝑋(Hom β€˜π‘‚)𝑃))
1347, 69, 10, 118, 11, 110, 37, 133nati 17902 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π‘Žβ€˜π‘ƒ)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹), ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ))((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)) = (((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹), ((1st β€˜πΉ)β€˜π‘‹)⟩(compβ€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ))(π‘Žβ€˜π‘‹)))
135123adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹) ∈ π‘ˆ)
13618, 40, 11, 135, 53, 61, 126, 73setcco 18029 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π‘Žβ€˜π‘ƒ)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹), ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ))((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)) = ((π‘Žβ€˜π‘ƒ) ∘ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)))
13759, 28ffvelcdmd 7084 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((1st β€˜πΉ)β€˜π‘‹) ∈ π‘ˆ)
138137adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((1st β€˜πΉ)β€˜π‘‹) ∈ π‘ˆ)
1397, 69, 10, 70, 110natcl 17900 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (π‘Žβ€˜π‘‹) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)(Hom β€˜π‘†)((1st β€˜πΉ)β€˜π‘‹)))
14018, 40, 70, 135, 138elsetchom 18027 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π‘Žβ€˜π‘‹) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)(Hom β€˜π‘†)((1st β€˜πΉ)β€˜π‘‹)) ↔ (π‘Žβ€˜π‘‹):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)⟢((1st β€˜πΉ)β€˜π‘‹)))
141139, 140mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (π‘Žβ€˜π‘‹):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)⟢((1st β€˜πΉ)β€˜π‘‹))
14210, 118, 70, 56, 28, 27funcf2 17814 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑋(2nd β€˜πΉ)𝑃):(𝑋(Hom β€˜π‘‚)𝑃)⟢(((1st β€˜πΉ)β€˜π‘‹)(Hom β€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ)))
143142, 121ffvelcdmd 7084 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ) ∈ (((1st β€˜πΉ)β€˜π‘‹)(Hom β€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ)))
14418, 22, 70, 137, 60elsetchom 18027 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ) ∈ (((1st β€˜πΉ)β€˜π‘‹)(Hom β€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ)) ↔ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ):((1st β€˜πΉ)β€˜π‘‹)⟢((1st β€˜πΉ)β€˜π‘ƒ)))
145143, 144mpbid 231 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ):((1st β€˜πΉ)β€˜π‘‹)⟢((1st β€˜πΉ)β€˜π‘ƒ))
146145adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ):((1st β€˜πΉ)β€˜π‘‹)⟢((1st β€˜πΉ)β€˜π‘ƒ))
14718, 40, 11, 135, 138, 61, 141, 146setcco 18029 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹), ((1st β€˜πΉ)β€˜π‘‹)⟩(compβ€˜π‘†)((1st β€˜πΉ)β€˜π‘ƒ))(π‘Žβ€˜π‘‹)) = (((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ) ∘ (π‘Žβ€˜π‘‹)))
148134, 136, 1473eqtr3d 2780 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π‘Žβ€˜π‘ƒ) ∘ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)) = (((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ) ∘ (π‘Žβ€˜π‘‹)))
149148fveq1d 6890 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((π‘Žβ€˜π‘ƒ) ∘ ((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ))β€˜( 1 β€˜π‘‹)) = ((((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ) ∘ (π‘Žβ€˜π‘‹))β€˜( 1 β€˜π‘‹)))
150127adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ( 1 β€˜π‘‹) ∈ (𝑋(Hom β€˜πΆ)𝑋))
15116, 9, 109, 110, 13, 110, 111, 37, 112, 150yon12 18214 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)β€˜( 1 β€˜π‘‹)) = (( 1 β€˜π‘‹)(βŸ¨π‘ƒ, π‘‹βŸ©(compβ€˜πΆ)𝑋)𝐾))
1529, 13, 99, 109, 37, 111, 110, 112catlid 17623 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (( 1 β€˜π‘‹)(βŸ¨π‘ƒ, π‘‹βŸ©(compβ€˜πΆ)𝑋)𝐾) = 𝐾)
153151, 152eqtrd 2772 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)β€˜( 1 β€˜π‘‹)) = 𝐾)
154153fveq2d 6892 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π‘Žβ€˜π‘ƒ)β€˜(((𝑋(2nd β€˜((1st β€˜π‘Œ)β€˜π‘‹))𝑃)β€˜πΎ)β€˜( 1 β€˜π‘‹))) = ((π‘Žβ€˜π‘ƒ)β€˜πΎ))
155132, 149, 1543eqtr3d 2780 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ) ∘ (π‘Žβ€˜π‘‹))β€˜( 1 β€˜π‘‹)) = ((π‘Žβ€˜π‘ƒ)β€˜πΎ))
156 fvco3 6987 . . . . . . . . . 10 (((π‘Žβ€˜π‘‹):((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)⟢((1st β€˜πΉ)β€˜π‘‹) ∧ ( 1 β€˜π‘‹) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘‹))β€˜π‘‹)) β†’ ((((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ) ∘ (π‘Žβ€˜π‘‹))β€˜( 1 β€˜π‘‹)) = (((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))))
157141, 130, 156syl2anc 584 . . . . . . . . 9 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ) ∘ (π‘Žβ€˜π‘‹))β€˜( 1 β€˜π‘‹)) = (((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))))
158117, 155, 1573eqtr2d 2778 . . . . . . . 8 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π‘Žβ€˜π‘ƒ)β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) = (((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))))
159158fveq2d 6892 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((π΄β€˜π‘ƒ)β€˜((π‘Žβ€˜π‘ƒ)β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)))) = ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹)))))
160108, 159eqtrd 2772 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ (((π΄β€˜π‘ƒ) ∘ (π‘Žβ€˜π‘ƒ))β€˜((((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) = ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹)))))
16198, 105, 1603eqtrd 2776 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)) β†’ ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)) = ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹)))))
162161mpteq2dva 5247 . . . 4 (πœ‘ β†’ (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)π‘Ž)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))))))
1635, 162eqtrid 2784 . . 3 (πœ‘ β†’ (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))))))
164 eqid 2732 . . . . . . . . . . 11 (𝑄 Γ—c 𝑂) = (𝑄 Γ—c 𝑂)
165164, 43, 10xpcbas 18126 . . . . . . . . . 10 ((𝑂 Func 𝑆) Γ— 𝐡) = (Baseβ€˜(𝑄 Γ—c 𝑂))
166 eqid 2732 . . . . . . . . . 10 (Hom β€˜(𝑄 Γ—c 𝑂)) = (Hom β€˜(𝑄 Γ—c 𝑂))
167 eqid 2732 . . . . . . . . . 10 (Hom β€˜π‘‡) = (Hom β€˜π‘‡)
168 relfunc 17808 . . . . . . . . . . 11 Rel ((𝑄 Γ—c 𝑂) Func 𝑇)
169 yoneda.t . . . . . . . . . . . . 13 𝑇 = (SetCatβ€˜π‘‰)
170 yoneda.h . . . . . . . . . . . . 13 𝐻 = (HomFβ€˜π‘„)
171 yoneda.r . . . . . . . . . . . . 13 𝑅 = ((𝑄 Γ—c 𝑂) FuncCat 𝑇)
172 yoneda.e . . . . . . . . . . . . 13 𝐸 = (𝑂 evalF 𝑆)
173 yoneda.z . . . . . . . . . . . . 13 𝑍 = (𝐻 ∘func ((⟨(1st β€˜π‘Œ), tpos (2nd β€˜π‘Œ)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
17416, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20yonedalem1 18221 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑍 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇)))
175174simpld 495 . . . . . . . . . . 11 (πœ‘ β†’ 𝑍 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇))
176 1st2ndbr 8024 . . . . . . . . . . 11 ((Rel ((𝑄 Γ—c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇)) β†’ (1st β€˜π‘)((𝑄 Γ—c 𝑂) Func 𝑇)(2nd β€˜π‘))
177168, 175, 176sylancr 587 . . . . . . . . . 10 (πœ‘ β†’ (1st β€˜π‘)((𝑄 Γ—c 𝑂) Func 𝑇)(2nd β€˜π‘))
17854, 28opelxpd 5713 . . . . . . . . . 10 (πœ‘ β†’ ⟨𝐹, π‘‹βŸ© ∈ ((𝑂 Func 𝑆) Γ— 𝐡))
17962, 27opelxpd 5713 . . . . . . . . . 10 (πœ‘ β†’ ⟨𝐺, π‘ƒβŸ© ∈ ((𝑂 Func 𝑆) Γ— 𝐡))
180165, 166, 167, 177, 178, 179funcf2 17814 . . . . . . . . 9 (πœ‘ β†’ (⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©):(⟨𝐹, π‘‹βŸ©(Hom β€˜(𝑄 Γ—c 𝑂))⟨𝐺, π‘ƒβŸ©)⟢(((1st β€˜π‘)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜π‘)β€˜βŸ¨πΊ, π‘ƒβŸ©)))
181164, 43, 10, 14, 118, 54, 28, 62, 27, 166xpchom2 18134 . . . . . . . . . . 11 (πœ‘ β†’ (⟨𝐹, π‘‹βŸ©(Hom β€˜(𝑄 Γ—c 𝑂))⟨𝐺, π‘ƒβŸ©) = ((𝐹(𝑂 Nat 𝑆)𝐺) Γ— (𝑋(Hom β€˜π‘‚)𝑃)))
182120xpeq2i 5702 . . . . . . . . . . 11 ((𝐹(𝑂 Nat 𝑆)𝐺) Γ— (𝑋(Hom β€˜π‘‚)𝑃)) = ((𝐹(𝑂 Nat 𝑆)𝐺) Γ— (𝑃(Hom β€˜πΆ)𝑋))
183181, 182eqtrdi 2788 . . . . . . . . . 10 (πœ‘ β†’ (⟨𝐹, π‘‹βŸ©(Hom β€˜(𝑄 Γ—c 𝑂))⟨𝐺, π‘ƒβŸ©) = ((𝐹(𝑂 Nat 𝑆)𝐺) Γ— (𝑃(Hom β€˜πΆ)𝑋)))
184 df-ov 7408 . . . . . . . . . . . . 13 (𝐹(1st β€˜π‘)𝑋) = ((1st β€˜π‘)β€˜βŸ¨πΉ, π‘‹βŸ©)
185 df-ov 7408 . . . . . . . . . . . . 13 (𝐺(1st β€˜π‘)𝑃) = ((1st β€˜π‘)β€˜βŸ¨πΊ, π‘ƒβŸ©)
186184, 185oveq12i 7417 . . . . . . . . . . . 12 ((𝐹(1st β€˜π‘)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜π‘)𝑃)) = (((1st β€˜π‘)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜π‘)β€˜βŸ¨πΊ, π‘ƒβŸ©))
187186eqcomi 2741 . . . . . . . . . . 11 (((1st β€˜π‘)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜π‘)β€˜βŸ¨πΊ, π‘ƒβŸ©)) = ((𝐹(1st β€˜π‘)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜π‘)𝑃))
188187a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (((1st β€˜π‘)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜π‘)β€˜βŸ¨πΊ, π‘ƒβŸ©)) = ((𝐹(1st β€˜π‘)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜π‘)𝑃)))
189183, 188feq23d 6709 . . . . . . . . 9 (πœ‘ β†’ ((⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©):(⟨𝐹, π‘‹βŸ©(Hom β€˜(𝑄 Γ—c 𝑂))⟨𝐺, π‘ƒβŸ©)⟢(((1st β€˜π‘)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜π‘)β€˜βŸ¨πΊ, π‘ƒβŸ©)) ↔ (⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©):((𝐹(𝑂 Nat 𝑆)𝐺) Γ— (𝑃(Hom β€˜πΆ)𝑋))⟢((𝐹(1st β€˜π‘)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜π‘)𝑃))))
190180, 189mpbid 231 . . . . . . . 8 (πœ‘ β†’ (⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©):((𝐹(𝑂 Nat 𝑆)𝐺) Γ— (𝑃(Hom β€˜πΆ)𝑋))⟢((𝐹(1st β€˜π‘)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜π‘)𝑃)))
191190, 34, 30fovcdmd 7575 . . . . . . 7 (πœ‘ β†’ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾) ∈ ((𝐹(1st β€˜π‘)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜π‘)𝑃)))
192 eqid 2732 . . . . . . . . . . 11 (Baseβ€˜π‘‡) = (Baseβ€˜π‘‡)
193165, 192, 177funcf1 17812 . . . . . . . . . 10 (πœ‘ β†’ (1st β€˜π‘):((𝑂 Func 𝑆) Γ— 𝐡)⟢(Baseβ€˜π‘‡))
194193, 54, 28fovcdmd 7575 . . . . . . . . 9 (πœ‘ β†’ (𝐹(1st β€˜π‘)𝑋) ∈ (Baseβ€˜π‘‡))
195169, 19setcbas 18024 . . . . . . . . 9 (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘‡))
196194, 195eleqtrrd 2836 . . . . . . . 8 (πœ‘ β†’ (𝐹(1st β€˜π‘)𝑋) ∈ 𝑉)
197193, 62, 27fovcdmd 7575 . . . . . . . . 9 (πœ‘ β†’ (𝐺(1st β€˜π‘)𝑃) ∈ (Baseβ€˜π‘‡))
198197, 195eleqtrrd 2836 . . . . . . . 8 (πœ‘ β†’ (𝐺(1st β€˜π‘)𝑃) ∈ 𝑉)
199169, 19, 167, 196, 198elsetchom 18027 . . . . . . 7 (πœ‘ β†’ ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾) ∈ ((𝐹(1st β€˜π‘)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜π‘)𝑃)) ↔ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾):(𝐹(1st β€˜π‘)𝑋)⟢(𝐺(1st β€˜π‘)𝑃)))
200191, 199mpbid 231 . . . . . 6 (πœ‘ β†’ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾):(𝐹(1st β€˜π‘)𝑋)⟢(𝐺(1st β€˜π‘)𝑃))
20116, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 62, 27, 34, 30yonedalem22 18227 . . . . . . . 8 (πœ‘ β†’ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾) = (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(2nd β€˜π»)⟨((1st β€˜π‘Œ)β€˜π‘ƒ), 𝐺⟩)𝐴))
2028oppccat 17664 . . . . . . . . . . 11 (𝐢 ∈ Cat β†’ 𝑂 ∈ Cat)
20317, 202syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑂 ∈ Cat)
20418setccat 18031 . . . . . . . . . . 11 (π‘ˆ ∈ V β†’ 𝑆 ∈ Cat)
20522, 204syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 ∈ Cat)
2066, 203, 205fuccat 17919 . . . . . . . . 9 (πœ‘ β†’ 𝑄 ∈ Cat)
207170, 206, 43, 14, 45, 54, 82, 62, 12, 31, 34hof2val 18205 . . . . . . . 8 (πœ‘ β†’ (((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(2nd β€˜π»)⟨((1st β€˜π‘Œ)β€˜π‘ƒ), 𝐺⟩)𝐴) = (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))))
208201, 207eqtrd 2772 . . . . . . 7 (πœ‘ β†’ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾) = (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))))
20916, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28yonedalem21 18222 . . . . . . 7 (πœ‘ β†’ (𝐹(1st β€˜π‘)𝑋) = (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹))
21016, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27yonedalem21 18222 . . . . . . 7 (πœ‘ β†’ (𝐺(1st β€˜π‘)𝑃) = (((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)𝐺))
211208, 209, 210feq123d 6703 . . . . . 6 (πœ‘ β†’ ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾):(𝐹(1st β€˜π‘)𝑋)⟢(𝐺(1st β€˜π‘)𝑃) ↔ (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))):(((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)⟢(((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)𝐺)))
212200, 211mpbid 231 . . . . 5 (πœ‘ β†’ (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))):(((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)⟢(((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)𝐺))
213 eqid 2732 . . . . . 6 (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))) = (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)))
214213fmpt 7106 . . . . 5 (βˆ€π‘ ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)) ∈ (((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)𝐺) ↔ (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))):(((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)⟢(((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)𝐺))
215212, 214sylibr 233 . . . 4 (πœ‘ β†’ βˆ€π‘ ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)) ∈ (((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)𝐺))
216 yonedalem3.m . . . . . 6 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), π‘₯ ∈ 𝐡 ↦ (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘₯)(𝑂 Nat 𝑆)𝑓) ↦ ((π‘Žβ€˜π‘₯)β€˜( 1 β€˜π‘₯))))
21716, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27, 216yonedalem3a 18223 . . . . 5 (πœ‘ β†’ ((𝐺𝑀𝑃) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)𝐺) ↦ ((π‘Žβ€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))) ∧ (𝐺𝑀𝑃):(𝐺(1st β€˜π‘)𝑃)⟢(𝐺(1st β€˜πΈ)𝑃)))
218217simpld 495 . . . 4 (πœ‘ β†’ (𝐺𝑀𝑃) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘ƒ)(𝑂 Nat 𝑆)𝐺) ↦ ((π‘Žβ€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))))
219 fveq1 6887 . . . . 5 (π‘Ž = ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)) β†’ (π‘Žβ€˜π‘ƒ) = (((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ))
220219fveq1d 6890 . . . 4 (π‘Ž = ((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ)) β†’ ((π‘Žβ€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)) = ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ)))
221215, 208, 218, 220fmptcof 7124 . . 3 (πœ‘ β†’ ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾)) = (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st β€˜π‘Œ)β€˜π‘‹), 𝐹⟩(compβ€˜π‘„)𝐺)𝑏)(⟨((1st β€˜π‘Œ)β€˜π‘ƒ), ((1st β€˜π‘Œ)β€˜π‘‹)⟩(compβ€˜π‘„)𝐺)((𝑃(2nd β€˜π‘Œ)𝑋)β€˜πΎ))β€˜π‘ƒ)β€˜( 1 β€˜π‘ƒ))))
222 eqid 2732 . . . . . . 7 (⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©) = (⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)
223172, 203, 205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121evlf2val 18168 . . . . . 6 (πœ‘ β†’ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾) = ((π΄β€˜π‘ƒ)(⟨((1st β€˜πΉ)β€˜π‘‹), ((1st β€˜πΉ)β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ))((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)))
22418, 22, 11, 137, 60, 67, 145, 77setcco 18029 . . . . . 6 (πœ‘ β†’ ((π΄β€˜π‘ƒ)(⟨((1st β€˜πΉ)β€˜π‘‹), ((1st β€˜πΉ)β€˜π‘ƒ)⟩(compβ€˜π‘†)((1st β€˜πΊ)β€˜π‘ƒ))((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)) = ((π΄β€˜π‘ƒ) ∘ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)))
225223, 224eqtrd 2772 . . . . 5 (πœ‘ β†’ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾) = ((π΄β€˜π‘ƒ) ∘ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)))
226225coeq1d 5859 . . . 4 (πœ‘ β†’ ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾) ∘ (𝐹𝑀𝑋)) = (((π΄β€˜π‘ƒ) ∘ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)) ∘ (𝐹𝑀𝑋)))
22716, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 216yonedalem3a 18223 . . . . . . . 8 (πœ‘ β†’ ((𝐹𝑀𝑋) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))) ∧ (𝐹𝑀𝑋):(𝐹(1st β€˜π‘)𝑋)⟢(𝐹(1st β€˜πΈ)𝑋)))
228227simprd 496 . . . . . . 7 (πœ‘ β†’ (𝐹𝑀𝑋):(𝐹(1st β€˜π‘)𝑋)⟢(𝐹(1st β€˜πΈ)𝑋))
229227simpld 495 . . . . . . . 8 (πœ‘ β†’ (𝐹𝑀𝑋) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))))
230172, 203, 205, 10, 54, 28evlf1 18169 . . . . . . . 8 (πœ‘ β†’ (𝐹(1st β€˜πΈ)𝑋) = ((1st β€˜πΉ)β€˜π‘‹))
231229, 209, 230feq123d 6703 . . . . . . 7 (πœ‘ β†’ ((𝐹𝑀𝑋):(𝐹(1st β€˜π‘)𝑋)⟢(𝐹(1st β€˜πΈ)𝑋) ↔ (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))):(((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)⟢((1st β€˜πΉ)β€˜π‘‹)))
232228, 231mpbid 231 . . . . . 6 (πœ‘ β†’ (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))):(((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)⟢((1st β€˜πΉ)β€˜π‘‹))
233 eqid 2732 . . . . . . 7 (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹)))
234233fmpt 7106 . . . . . 6 (βˆ€π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹)) ∈ ((1st β€˜πΉ)β€˜π‘‹) ↔ (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))):(((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)⟢((1st β€˜πΉ)β€˜π‘‹))
235232, 234sylibr 233 . . . . 5 (πœ‘ β†’ βˆ€π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹)((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹)) ∈ ((1st β€˜πΉ)β€˜π‘‹))
236 fcompt 7127 . . . . . 6 (((π΄β€˜π‘ƒ):((1st β€˜πΉ)β€˜π‘ƒ)⟢((1st β€˜πΊ)β€˜π‘ƒ) ∧ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ):((1st β€˜πΉ)β€˜π‘‹)⟢((1st β€˜πΉ)β€˜π‘ƒ)) β†’ ((π΄β€˜π‘ƒ) ∘ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)) = (𝑦 ∈ ((1st β€˜πΉ)β€˜π‘‹) ↦ ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜π‘¦))))
23777, 145, 236syl2anc 584 . . . . 5 (πœ‘ β†’ ((π΄β€˜π‘ƒ) ∘ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)) = (𝑦 ∈ ((1st β€˜πΉ)β€˜π‘‹) ↦ ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜π‘¦))))
238 2fveq3 6893 . . . . 5 (𝑦 = ((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹)) β†’ ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜π‘¦)) = ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹)))))
239235, 229, 237, 238fmptcof 7124 . . . 4 (πœ‘ β†’ (((π΄β€˜π‘ƒ) ∘ ((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)) ∘ (𝐹𝑀𝑋)) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))))))
240226, 239eqtrd 2772 . . 3 (πœ‘ β†’ ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾) ∘ (𝐹𝑀𝑋)) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘‹)(𝑂 Nat 𝑆)𝐹) ↦ ((π΄β€˜π‘ƒ)β€˜(((𝑋(2nd β€˜πΉ)𝑃)β€˜πΎ)β€˜((π‘Žβ€˜π‘‹)β€˜( 1 β€˜π‘‹))))))
241163, 221, 2403eqtr4d 2782 . 2 (πœ‘ β†’ ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾)) = ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾) ∘ (𝐹𝑀𝑋)))
242 eqid 2732 . . 3 (compβ€˜π‘‡) = (compβ€˜π‘‡)
243174simprd 496 . . . . . . 7 (πœ‘ β†’ 𝐸 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇))
244 1st2ndbr 8024 . . . . . . 7 ((Rel ((𝑄 Γ—c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇)) β†’ (1st β€˜πΈ)((𝑄 Γ—c 𝑂) Func 𝑇)(2nd β€˜πΈ))
245168, 243, 244sylancr 587 . . . . . 6 (πœ‘ β†’ (1st β€˜πΈ)((𝑄 Γ—c 𝑂) Func 𝑇)(2nd β€˜πΈ))
246165, 192, 245funcf1 17812 . . . . 5 (πœ‘ β†’ (1st β€˜πΈ):((𝑂 Func 𝑆) Γ— 𝐡)⟢(Baseβ€˜π‘‡))
247246, 62, 27fovcdmd 7575 . . . 4 (πœ‘ β†’ (𝐺(1st β€˜πΈ)𝑃) ∈ (Baseβ€˜π‘‡))
248247, 195eleqtrrd 2836 . . 3 (πœ‘ β†’ (𝐺(1st β€˜πΈ)𝑃) ∈ 𝑉)
249217simprd 496 . . 3 (πœ‘ β†’ (𝐺𝑀𝑃):(𝐺(1st β€˜π‘)𝑃)⟢(𝐺(1st β€˜πΈ)𝑃))
250169, 19, 242, 196, 198, 248, 200, 249setcco 18029 . 2 (πœ‘ β†’ ((𝐺𝑀𝑃)(⟨(𝐹(1st β€˜π‘)𝑋), (𝐺(1st β€˜π‘)𝑃)⟩(compβ€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃))(𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾)) = ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾)))
251246, 54, 28fovcdmd 7575 . . . 4 (πœ‘ β†’ (𝐹(1st β€˜πΈ)𝑋) ∈ (Baseβ€˜π‘‡))
252251, 195eleqtrrd 2836 . . 3 (πœ‘ β†’ (𝐹(1st β€˜πΈ)𝑋) ∈ 𝑉)
253165, 166, 167, 245, 178, 179funcf2 17814 . . . . . 6 (πœ‘ β†’ (⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©):(⟨𝐹, π‘‹βŸ©(Hom β€˜(𝑄 Γ—c 𝑂))⟨𝐺, π‘ƒβŸ©)⟢(((1st β€˜πΈ)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜πΈ)β€˜βŸ¨πΊ, π‘ƒβŸ©)))
254 df-ov 7408 . . . . . . . . . 10 (𝐹(1st β€˜πΈ)𝑋) = ((1st β€˜πΈ)β€˜βŸ¨πΉ, π‘‹βŸ©)
255 df-ov 7408 . . . . . . . . . 10 (𝐺(1st β€˜πΈ)𝑃) = ((1st β€˜πΈ)β€˜βŸ¨πΊ, π‘ƒβŸ©)
256254, 255oveq12i 7417 . . . . . . . . 9 ((𝐹(1st β€˜πΈ)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃)) = (((1st β€˜πΈ)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜πΈ)β€˜βŸ¨πΊ, π‘ƒβŸ©))
257256eqcomi 2741 . . . . . . . 8 (((1st β€˜πΈ)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜πΈ)β€˜βŸ¨πΊ, π‘ƒβŸ©)) = ((𝐹(1st β€˜πΈ)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃))
258257a1i 11 . . . . . . 7 (πœ‘ β†’ (((1st β€˜πΈ)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜πΈ)β€˜βŸ¨πΊ, π‘ƒβŸ©)) = ((𝐹(1st β€˜πΈ)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃)))
259183, 258feq23d 6709 . . . . . 6 (πœ‘ β†’ ((⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©):(⟨𝐹, π‘‹βŸ©(Hom β€˜(𝑄 Γ—c 𝑂))⟨𝐺, π‘ƒβŸ©)⟢(((1st β€˜πΈ)β€˜βŸ¨πΉ, π‘‹βŸ©)(Hom β€˜π‘‡)((1st β€˜πΈ)β€˜βŸ¨πΊ, π‘ƒβŸ©)) ↔ (⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©):((𝐹(𝑂 Nat 𝑆)𝐺) Γ— (𝑃(Hom β€˜πΆ)𝑋))⟢((𝐹(1st β€˜πΈ)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃))))
260253, 259mpbid 231 . . . . 5 (πœ‘ β†’ (⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©):((𝐹(𝑂 Nat 𝑆)𝐺) Γ— (𝑃(Hom β€˜πΆ)𝑋))⟢((𝐹(1st β€˜πΈ)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃)))
261260, 34, 30fovcdmd 7575 . . . 4 (πœ‘ β†’ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾) ∈ ((𝐹(1st β€˜πΈ)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃)))
262169, 19, 167, 252, 248elsetchom 18027 . . . 4 (πœ‘ β†’ ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾) ∈ ((𝐹(1st β€˜πΈ)𝑋)(Hom β€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃)) ↔ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾):(𝐹(1st β€˜πΈ)𝑋)⟢(𝐺(1st β€˜πΈ)𝑃)))
263261, 262mpbid 231 . . 3 (πœ‘ β†’ (𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾):(𝐹(1st β€˜πΈ)𝑋)⟢(𝐺(1st β€˜πΈ)𝑃))
264169, 19, 242, 196, 252, 248, 228, 263setcco 18029 . 2 (πœ‘ β†’ ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾)(⟨(𝐹(1st β€˜π‘)𝑋), (𝐹(1st β€˜πΈ)𝑋)⟩(compβ€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃))(𝐹𝑀𝑋)) = ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾) ∘ (𝐹𝑀𝑋)))
265241, 250, 2643eqtr4d 2782 1 (πœ‘ β†’ ((𝐺𝑀𝑃)(⟨(𝐹(1st β€˜π‘)𝑋), (𝐺(1st β€˜π‘)𝑃)⟩(compβ€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃))(𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜π‘)⟨𝐺, π‘ƒβŸ©)𝐾)) = ((𝐴(⟨𝐹, π‘‹βŸ©(2nd β€˜πΈ)⟨𝐺, π‘ƒβŸ©)𝐾)(⟨(𝐹(1st β€˜π‘)𝑋), (𝐹(1st β€˜πΈ)𝑋)⟩(compβ€˜π‘‡)(𝐺(1st β€˜πΈ)𝑃))(𝐹𝑀𝑋)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  Vcvv 3474   βˆͺ cun 3945   βŠ† wss 3947  βŸ¨cop 4633   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673  ran crn 5676   ∘ ccom 5679  Rel wrel 5680  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∈ cmpo 7407  1st c1st 7969  2nd c2nd 7970  tpos ctpos 8206  Basecbs 17140  Hom chom 17204  compcco 17205  Catccat 17604  Idccid 17605  Homf chomf 17606  oppCatcoppc 17651   Func cfunc 17800   ∘func ccofu 17802   Nat cnat 17888   FuncCat cfuc 17889  SetCatcsetc 18021   Γ—c cxpc 18116   1stF c1stf 18117   2ndF c2ndf 18118   ⟨,⟩F cprf 18119   evalF cevlf 18158  HomFchof 18197  Yoncyon 18198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-tpos 8207  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-fz 13481  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-hom 17217  df-cco 17218  df-cat 17608  df-cid 17609  df-homf 17610  df-comf 17611  df-oppc 17652  df-ssc 17753  df-resc 17754  df-subc 17755  df-func 17804  df-cofu 17806  df-nat 17890  df-fuc 17891  df-setc 18022  df-xpc 18120  df-1stf 18121  df-2ndf 18122  df-prf 18123  df-evlf 18162  df-curf 18163  df-hof 18199  df-yon 18200
This theorem is referenced by:  yonedalem3  18229
  Copyright terms: Public domain W3C validator