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

Theorem yonedainv 18246
Description: The Yoneda Lemma with explicit inverse. (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 β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
yoneda.m 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), π‘₯ ∈ 𝐡 ↦ (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘₯)(𝑂 Nat 𝑆)𝑓) ↦ ((π‘Žβ€˜π‘₯)β€˜( 1 β€˜π‘₯))))
yonedainv.i 𝐼 = (Invβ€˜π‘…)
yonedainv.n 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), π‘₯ ∈ 𝐡 ↦ (𝑒 ∈ ((1st β€˜π‘“)β€˜π‘₯) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)π‘₯) ↦ (((π‘₯(2nd β€˜π‘“)𝑦)β€˜π‘”)β€˜π‘’)))))
Assertion
Ref Expression
yonedainv (πœ‘ β†’ 𝑀(𝑍𝐼𝐸)𝑁)
Distinct variable groups:   𝑓,π‘Ž,𝑔,π‘₯,𝑦, 1   𝑒,π‘Ž,𝑔,𝑦,𝐢,𝑓,π‘₯   𝐸,π‘Ž,𝑓,𝑔,𝑒,𝑦   𝐡,π‘Ž,𝑓,𝑔,𝑒,π‘₯,𝑦   𝑁,π‘Ž   𝑂,π‘Ž,𝑓,𝑔,𝑒,π‘₯,𝑦   𝑆,π‘Ž,𝑓,𝑔,𝑒,π‘₯,𝑦   𝑔,𝑀,𝑒,𝑦   𝑄,π‘Ž,𝑓,𝑔,𝑒,π‘₯   𝑇,𝑓,𝑔,𝑒,𝑦   πœ‘,π‘Ž,𝑓,𝑔,𝑒,π‘₯,𝑦   𝑒,𝑅   π‘Œ,π‘Ž,𝑓,𝑔,𝑒,π‘₯,𝑦   𝑍,π‘Ž,𝑓,𝑔,𝑒,π‘₯,𝑦
Allowed substitution hints:   𝑄(𝑦)   𝑅(π‘₯,𝑦,𝑓,𝑔,π‘Ž)   𝑇(π‘₯,π‘Ž)   π‘ˆ(π‘₯,𝑦,𝑒,𝑓,𝑔,π‘Ž)   1 (𝑒)   𝐸(π‘₯)   𝐻(π‘₯,𝑦,𝑒,𝑓,𝑔,π‘Ž)   𝐼(π‘₯,𝑦,𝑒,𝑓,𝑔,π‘Ž)   𝑀(π‘₯,𝑓,π‘Ž)   𝑁(π‘₯,𝑦,𝑒,𝑓,𝑔)   𝑉(π‘₯,𝑦,𝑒,𝑓,𝑔,π‘Ž)   π‘Š(π‘₯,𝑦,𝑒,𝑓,𝑔,π‘Ž)

Proof of Theorem yonedainv
Dummy variables 𝑏 β„Ž π‘˜ 𝑀 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 yoneda.r . . 3 𝑅 = ((𝑄 Γ—c 𝑂) FuncCat 𝑇)
2 eqid 2726 . . . 4 (𝑄 Γ—c 𝑂) = (𝑄 Γ—c 𝑂)
3 yoneda.q . . . . 5 𝑄 = (𝑂 FuncCat 𝑆)
43fucbas 17924 . . . 4 (𝑂 Func 𝑆) = (Baseβ€˜π‘„)
5 yoneda.o . . . . 5 𝑂 = (oppCatβ€˜πΆ)
6 yoneda.b . . . . 5 𝐡 = (Baseβ€˜πΆ)
75, 6oppcbas 17672 . . . 4 𝐡 = (Baseβ€˜π‘‚)
82, 4, 7xpcbas 18142 . . 3 ((𝑂 Func 𝑆) Γ— 𝐡) = (Baseβ€˜(𝑄 Γ—c 𝑂))
9 eqid 2726 . . 3 ((𝑄 Γ—c 𝑂) Nat 𝑇) = ((𝑄 Γ—c 𝑂) Nat 𝑇)
10 yoneda.y . . . . 5 π‘Œ = (Yonβ€˜πΆ)
11 yoneda.1 . . . . 5 1 = (Idβ€˜πΆ)
12 yoneda.s . . . . 5 𝑆 = (SetCatβ€˜π‘ˆ)
13 yoneda.t . . . . 5 𝑇 = (SetCatβ€˜π‘‰)
14 yoneda.h . . . . 5 𝐻 = (HomFβ€˜π‘„)
15 yoneda.e . . . . 5 𝐸 = (𝑂 evalF 𝑆)
16 yoneda.z . . . . 5 𝑍 = (𝐻 ∘func ((⟨(1st β€˜π‘Œ), tpos (2nd β€˜π‘Œ)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
17 yoneda.c . . . . 5 (πœ‘ β†’ 𝐢 ∈ Cat)
18 yoneda.w . . . . 5 (πœ‘ β†’ 𝑉 ∈ π‘Š)
19 yoneda.u . . . . 5 (πœ‘ β†’ ran (Homf β€˜πΆ) βŠ† π‘ˆ)
20 yoneda.v . . . . 5 (πœ‘ β†’ (ran (Homf β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
2110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20yonedalem1 18237 . . . 4 (πœ‘ β†’ (𝑍 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇)))
2221simpld 494 . . 3 (πœ‘ β†’ 𝑍 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇))
2321simprd 495 . . 3 (πœ‘ β†’ 𝐸 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇))
24 yonedainv.i . . 3 𝐼 = (Invβ€˜π‘…)
25 eqid 2726 . . 3 (Invβ€˜π‘‡) = (Invβ€˜π‘‡)
26 yoneda.m . . . 4 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), π‘₯ ∈ 𝐡 ↦ (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘₯)(𝑂 Nat 𝑆)𝑓) ↦ ((π‘Žβ€˜π‘₯)β€˜( 1 β€˜π‘₯))))
2710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26yonedalem3 18245 . . 3 (πœ‘ β†’ 𝑀 ∈ (𝑍((𝑄 Γ—c 𝑂) Nat 𝑇)𝐸))
2817adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ 𝐢 ∈ Cat)
2918adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ 𝑉 ∈ π‘Š)
3019adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ran (Homf β€˜πΆ) βŠ† π‘ˆ)
3120adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (ran (Homf β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
32 simprl 768 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ β„Ž ∈ (𝑂 Func 𝑆))
33 simprr 770 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ 𝑀 ∈ 𝐡)
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 18239 . . . . . . . . . 10 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘€π‘€) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€))) ∧ (β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢(β„Ž(1st β€˜πΈ)𝑀)))
3534simprd 495 . . . . . . . . 9 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢(β„Ž(1st β€˜πΈ)𝑀))
3628adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ 𝐢 ∈ Cat)
3729adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ 𝑉 ∈ π‘Š)
3830adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ran (Homf β€˜πΆ) βŠ† π‘ˆ)
3931adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (ran (Homf β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
40 simplrl 774 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ β„Ž ∈ (𝑂 Func 𝑆))
41 simplrr 775 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ 𝑀 ∈ 𝐡)
42 yonedainv.n . . . . . . . . . . . 12 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), π‘₯ ∈ 𝐡 ↦ (𝑒 ∈ ((1st β€˜π‘“)β€˜π‘₯) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)π‘₯) ↦ (((π‘₯(2nd β€˜π‘“)𝑦)β€˜π‘”)β€˜π‘’)))))
43 simpr 484 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€))
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 18242 . . . . . . . . . . 11 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((β„Žπ‘π‘€)β€˜π‘) ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž))
4544fmpttd 7110 . . . . . . . . . 10 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ ((β„Žπ‘π‘€)β€˜π‘)):((1st β€˜β„Ž)β€˜π‘€)⟢(((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž))
466fvexi 6899 . . . . . . . . . . . . . . 15 𝐡 ∈ V
4746mptex 7220 . . . . . . . . . . . . . 14 (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’))) ∈ V
48 eqid 2726 . . . . . . . . . . . . . 14 (𝑒 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’)))) = (𝑒 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’))))
4947, 48fnmpti 6687 . . . . . . . . . . . . 13 (𝑒 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’)))) Fn ((1st β€˜β„Ž)β€˜π‘€)
50 simpl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = β„Ž ∧ π‘₯ = 𝑀) β†’ 𝑓 = β„Ž)
5150fveq2d 6889 . . . . . . . . . . . . . . . . . 18 ((𝑓 = β„Ž ∧ π‘₯ = 𝑀) β†’ (1st β€˜π‘“) = (1st β€˜β„Ž))
52 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝑓 = β„Ž ∧ π‘₯ = 𝑀) β†’ π‘₯ = 𝑀)
5351, 52fveq12d 6892 . . . . . . . . . . . . . . . . 17 ((𝑓 = β„Ž ∧ π‘₯ = 𝑀) β†’ ((1st β€˜π‘“)β€˜π‘₯) = ((1st β€˜β„Ž)β€˜π‘€))
54 simplr 766 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ π‘₯ = 𝑀)
5554oveq2d 7421 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ (𝑦(Hom β€˜πΆ)π‘₯) = (𝑦(Hom β€˜πΆ)𝑀))
56 simpll 764 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ 𝑓 = β„Ž)
5756fveq2d 6889 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ (2nd β€˜π‘“) = (2nd β€˜β„Ž))
58 eqidd 2727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 = 𝑦)
5957, 54, 58oveq123d 7426 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ (π‘₯(2nd β€˜π‘“)𝑦) = (𝑀(2nd β€˜β„Ž)𝑦))
6059fveq1d 6887 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ ((π‘₯(2nd β€˜π‘“)𝑦)β€˜π‘”) = ((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”))
6160fveq1d 6887 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ (((π‘₯(2nd β€˜π‘“)𝑦)β€˜π‘”)β€˜π‘’) = (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’))
6255, 61mpteq12dv 5232 . . . . . . . . . . . . . . . . . 18 (((𝑓 = β„Ž ∧ π‘₯ = 𝑀) ∧ 𝑦 ∈ 𝐡) β†’ (𝑔 ∈ (𝑦(Hom β€˜πΆ)π‘₯) ↦ (((π‘₯(2nd β€˜π‘“)𝑦)β€˜π‘”)β€˜π‘’)) = (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’)))
6362mpteq2dva 5241 . . . . . . . . . . . . . . . . 17 ((𝑓 = β„Ž ∧ π‘₯ = 𝑀) β†’ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)π‘₯) ↦ (((π‘₯(2nd β€˜π‘“)𝑦)β€˜π‘”)β€˜π‘’))) = (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’))))
6453, 63mpteq12dv 5232 . . . . . . . . . . . . . . . 16 ((𝑓 = β„Ž ∧ π‘₯ = 𝑀) β†’ (𝑒 ∈ ((1st β€˜π‘“)β€˜π‘₯) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)π‘₯) ↦ (((π‘₯(2nd β€˜π‘“)𝑦)β€˜π‘”)β€˜π‘’)))) = (𝑒 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’)))))
65 fvex 6898 . . . . . . . . . . . . . . . . 17 ((1st β€˜β„Ž)β€˜π‘€) ∈ V
6665mptex 7220 . . . . . . . . . . . . . . . 16 (𝑒 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’)))) ∈ V
6764, 42, 66ovmpoa 7559 . . . . . . . . . . . . . . 15 ((β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡) β†’ (β„Žπ‘π‘€) = (𝑒 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’)))))
6867adantl 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Žπ‘π‘€) = (𝑒 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’)))))
6968fneq1d 6636 . . . . . . . . . . . . 13 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘π‘€) Fn ((1st β€˜β„Ž)β€˜π‘€) ↔ (𝑒 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)𝑀) ↦ (((𝑀(2nd β€˜β„Ž)𝑦)β€˜π‘”)β€˜π‘’)))) Fn ((1st β€˜β„Ž)β€˜π‘€)))
7049, 69mpbiri 258 . . . . . . . . . . . 12 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Žπ‘π‘€) Fn ((1st β€˜β„Ž)β€˜π‘€))
71 dffn5 6944 . . . . . . . . . . . 12 ((β„Žπ‘π‘€) Fn ((1st β€˜β„Ž)β€˜π‘€) ↔ (β„Žπ‘π‘€) = (𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ ((β„Žπ‘π‘€)β€˜π‘)))
7270, 71sylib 217 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Žπ‘π‘€) = (𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ ((β„Žπ‘π‘€)β€˜π‘)))
735oppccat 17677 . . . . . . . . . . . . . 14 (𝐢 ∈ Cat β†’ 𝑂 ∈ Cat)
7417, 73syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑂 ∈ Cat)
7574adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ 𝑂 ∈ Cat)
7620unssbd 4183 . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘ˆ βŠ† 𝑉)
7718, 76ssexd 5317 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘ˆ ∈ V)
7812setccat 18047 . . . . . . . . . . . . . 14 (π‘ˆ ∈ V β†’ 𝑆 ∈ Cat)
7977, 78syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 ∈ Cat)
8079adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ 𝑆 ∈ Cat)
8115, 75, 80, 7, 32, 33evlf1 18185 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Ž(1st β€˜πΈ)𝑀) = ((1st β€˜β„Ž)β€˜π‘€))
8210, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 18238 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Ž(1st β€˜π‘)𝑀) = (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž))
8372, 81, 82feq123d 6700 . . . . . . . . . 10 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘π‘€):(β„Ž(1st β€˜πΈ)𝑀)⟢(β„Ž(1st β€˜π‘)𝑀) ↔ (𝑏 ∈ ((1st β€˜β„Ž)β€˜π‘€) ↦ ((β„Žπ‘π‘€)β€˜π‘)):((1st β€˜β„Ž)β€˜π‘€)⟢(((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž)))
8445, 83mpbird 257 . . . . . . . . 9 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Žπ‘π‘€):(β„Ž(1st β€˜πΈ)𝑀)⟢(β„Ž(1st β€˜π‘)𝑀))
85 fcompt 7127 . . . . . . . . . . 11 (((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢(β„Ž(1st β€˜πΈ)𝑀) ∧ (β„Žπ‘π‘€):(β„Ž(1st β€˜πΈ)𝑀)⟢(β„Ž(1st β€˜π‘)𝑀)) β†’ ((β„Žπ‘€π‘€) ∘ (β„Žπ‘π‘€)) = (π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀) ↦ ((β„Žπ‘€π‘€)β€˜((β„Žπ‘π‘€)β€˜π‘˜))))
8635, 84, 85syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘€π‘€) ∘ (β„Žπ‘π‘€)) = (π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀) ↦ ((β„Žπ‘€π‘€)β€˜((β„Žπ‘π‘€)β€˜π‘˜))))
8781eleq2d 2813 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀) ↔ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)))
8887biimpa 476 . . . . . . . . . . . . 13 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀)) β†’ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€))
8928adantr 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ 𝐢 ∈ Cat)
9029adantr 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ 𝑉 ∈ π‘Š)
9130adantr 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ran (Homf β€˜πΆ) βŠ† π‘ˆ)
9231adantr 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (ran (Homf β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
93 simplrl 774 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ β„Ž ∈ (𝑂 Func 𝑆))
94 simplrr 775 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ 𝑀 ∈ 𝐡)
9510, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 26yonedalem3a 18239 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((β„Žπ‘€π‘€) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€))) ∧ (β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢(β„Ž(1st β€˜πΈ)𝑀)))
9695simpld 494 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (β„Žπ‘€π‘€) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€))))
9796fveq1d 6887 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((β„Žπ‘€π‘€)β€˜((β„Žπ‘π‘€)β€˜π‘˜)) = ((π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)))β€˜((β„Žπ‘π‘€)β€˜π‘˜)))
9872, 44fmpt3d 7111 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Žπ‘π‘€):((1st β€˜β„Ž)β€˜π‘€)⟢(((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž))
9998ffvelcdmda 7080 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((β„Žπ‘π‘€)β€˜π‘˜) ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž))
100 fveq1 6884 . . . . . . . . . . . . . . . . 17 (π‘Ž = ((β„Žπ‘π‘€)β€˜π‘˜) β†’ (π‘Žβ€˜π‘€) = (((β„Žπ‘π‘€)β€˜π‘˜)β€˜π‘€))
101100fveq1d 6887 . . . . . . . . . . . . . . . 16 (π‘Ž = ((β„Žπ‘π‘€)β€˜π‘˜) β†’ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)) = ((((β„Žπ‘π‘€)β€˜π‘˜)β€˜π‘€)β€˜( 1 β€˜π‘€)))
102 eqid 2726 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€))) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)))
103 fvex 6898 . . . . . . . . . . . . . . . 16 ((((β„Žπ‘π‘€)β€˜π‘˜)β€˜π‘€)β€˜( 1 β€˜π‘€)) ∈ V
104101, 102, 103fvmpt 6992 . . . . . . . . . . . . . . 15 (((β„Žπ‘π‘€)β€˜π‘˜) ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) β†’ ((π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)))β€˜((β„Žπ‘π‘€)β€˜π‘˜)) = ((((β„Žπ‘π‘€)β€˜π‘˜)β€˜π‘€)β€˜( 1 β€˜π‘€)))
10599, 104syl 17 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)))β€˜((β„Žπ‘π‘€)β€˜π‘˜)) = ((((β„Žπ‘π‘€)β€˜π‘˜)β€˜π‘€)β€˜( 1 β€˜π‘€)))
106 simpr 484 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€))
107 eqid 2726 . . . . . . . . . . . . . . . . 17 (Hom β€˜πΆ) = (Hom β€˜πΆ)
1086, 107, 11, 89, 94catidcl 17635 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ( 1 β€˜π‘€) ∈ (𝑀(Hom β€˜πΆ)𝑀))
10910, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 42, 106, 94, 108yonedalem4b 18241 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((((β„Žπ‘π‘€)β€˜π‘˜)β€˜π‘€)β€˜( 1 β€˜π‘€)) = (((𝑀(2nd β€˜β„Ž)𝑀)β€˜( 1 β€˜π‘€))β€˜π‘˜))
110 eqid 2726 . . . . . . . . . . . . . . . . . 18 (Idβ€˜π‘‚) = (Idβ€˜π‘‚)
111 eqid 2726 . . . . . . . . . . . . . . . . . 18 (Idβ€˜π‘†) = (Idβ€˜π‘†)
112 relfunc 17821 . . . . . . . . . . . . . . . . . . 19 Rel (𝑂 Func 𝑆)
113 1st2ndbr 8027 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝑂 Func 𝑆) ∧ β„Ž ∈ (𝑂 Func 𝑆)) β†’ (1st β€˜β„Ž)(𝑂 Func 𝑆)(2nd β€˜β„Ž))
114112, 93, 113sylancr 586 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (1st β€˜β„Ž)(𝑂 Func 𝑆)(2nd β€˜β„Ž))
1157, 110, 111, 114, 94funcid 17829 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((𝑀(2nd β€˜β„Ž)𝑀)β€˜((Idβ€˜π‘‚)β€˜π‘€)) = ((Idβ€˜π‘†)β€˜((1st β€˜β„Ž)β€˜π‘€)))
1165, 11oppcid 17676 . . . . . . . . . . . . . . . . . . . 20 (𝐢 ∈ Cat β†’ (Idβ€˜π‘‚) = 1 )
11789, 116syl 17 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (Idβ€˜π‘‚) = 1 )
118117fveq1d 6887 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((Idβ€˜π‘‚)β€˜π‘€) = ( 1 β€˜π‘€))
119118fveq2d 6889 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((𝑀(2nd β€˜β„Ž)𝑀)β€˜((Idβ€˜π‘‚)β€˜π‘€)) = ((𝑀(2nd β€˜β„Ž)𝑀)β€˜( 1 β€˜π‘€)))
12077ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ π‘ˆ ∈ V)
121 eqid 2726 . . . . . . . . . . . . . . . . . . . . 21 (Baseβ€˜π‘†) = (Baseβ€˜π‘†)
1227, 121, 114funcf1 17825 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (1st β€˜β„Ž):𝐡⟢(Baseβ€˜π‘†))
12312, 120setcbas 18040 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ π‘ˆ = (Baseβ€˜π‘†))
124123feq3d 6698 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((1st β€˜β„Ž):π΅βŸΆπ‘ˆ ↔ (1st β€˜β„Ž):𝐡⟢(Baseβ€˜π‘†)))
125122, 124mpbird 257 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (1st β€˜β„Ž):π΅βŸΆπ‘ˆ)
126125, 94ffvelcdmd 7081 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((1st β€˜β„Ž)β€˜π‘€) ∈ π‘ˆ)
12712, 111, 120, 126setcid 18048 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((Idβ€˜π‘†)β€˜((1st β€˜β„Ž)β€˜π‘€)) = ( I β†Ύ ((1st β€˜β„Ž)β€˜π‘€)))
128115, 119, 1273eqtr3d 2774 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((𝑀(2nd β€˜β„Ž)𝑀)β€˜( 1 β€˜π‘€)) = ( I β†Ύ ((1st β€˜β„Ž)β€˜π‘€)))
129128fveq1d 6887 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (((𝑀(2nd β€˜β„Ž)𝑀)β€˜( 1 β€˜π‘€))β€˜π‘˜) = (( I β†Ύ ((1st β€˜β„Ž)β€˜π‘€))β€˜π‘˜))
130 fvresi 7167 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€) β†’ (( I β†Ύ ((1st β€˜β„Ž)β€˜π‘€))β€˜π‘˜) = π‘˜)
131130adantl 481 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ (( I β†Ύ ((1st β€˜β„Ž)β€˜π‘€))β€˜π‘˜) = π‘˜)
132109, 129, 1313eqtrd 2770 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((((β„Žπ‘π‘€)β€˜π‘˜)β€˜π‘€)β€˜( 1 β€˜π‘€)) = π‘˜)
13397, 105, 1323eqtrd 2770 . . . . . . . . . . . . 13 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ ((1st β€˜β„Ž)β€˜π‘€)) β†’ ((β„Žπ‘€π‘€)β€˜((β„Žπ‘π‘€)β€˜π‘˜)) = π‘˜)
13488, 133syldan 590 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀)) β†’ ((β„Žπ‘€π‘€)β€˜((β„Žπ‘π‘€)β€˜π‘˜)) = π‘˜)
135134mpteq2dva 5241 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀) ↦ ((β„Žπ‘€π‘€)β€˜((β„Žπ‘π‘€)β€˜π‘˜))) = (π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀) ↦ π‘˜))
136 mptresid 6044 . . . . . . . . . . 11 ( I β†Ύ (β„Ž(1st β€˜πΈ)𝑀)) = (π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀) ↦ π‘˜)
137135, 136eqtr4di 2784 . . . . . . . . . 10 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (π‘˜ ∈ (β„Ž(1st β€˜πΈ)𝑀) ↦ ((β„Žπ‘€π‘€)β€˜((β„Žπ‘π‘€)β€˜π‘˜))) = ( I β†Ύ (β„Ž(1st β€˜πΈ)𝑀)))
13886, 137eqtrd 2766 . . . . . . . . 9 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘€π‘€) ∘ (β„Žπ‘π‘€)) = ( I β†Ύ (β„Ž(1st β€˜πΈ)𝑀)))
139 fcompt 7127 . . . . . . . . . . 11 (((β„Žπ‘π‘€):(β„Ž(1st β€˜πΈ)𝑀)⟢(β„Ž(1st β€˜π‘)𝑀) ∧ (β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢(β„Ž(1st β€˜πΈ)𝑀)) β†’ ((β„Žπ‘π‘€) ∘ (β„Žπ‘€π‘€)) = (𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀) ↦ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))))
14084, 35, 139syl2anc 583 . . . . . . . . . 10 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘π‘€) ∘ (β„Žπ‘€π‘€)) = (𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀) ↦ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))))
141 eqid 2726 . . . . . . . . . . . . . 14 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
14228adantr 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ 𝐢 ∈ Cat)
14329adantr 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ 𝑉 ∈ π‘Š)
14430adantr 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ran (Homf β€˜πΆ) βŠ† π‘ˆ)
14531adantr 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (ran (Homf β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
146 simplrl 774 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ β„Ž ∈ (𝑂 Func 𝑆))
147 simplrr 775 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ 𝑀 ∈ 𝐡)
14881feq3d 6698 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢(β„Ž(1st β€˜πΈ)𝑀) ↔ (β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢((1st β€˜β„Ž)β€˜π‘€)))
14935, 148mpbid 231 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢((1st β€˜β„Ž)β€˜π‘€))
150149ffvelcdmda 7080 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((β„Žπ‘€π‘€)β€˜π‘) ∈ ((1st β€˜β„Ž)β€˜π‘€))
15110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 142, 143, 144, 145, 146, 147, 42, 150yonedalem4c 18242 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘)) ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž))
152141, 151nat1st2nd 17914 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘)) ∈ (⟨(1st β€˜((1st β€˜π‘Œ)β€˜π‘€)), (2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))⟩(𝑂 Nat 𝑆)⟨(1st β€˜β„Ž), (2nd β€˜β„Ž)⟩))
153141, 152, 7natfn 17917 . . . . . . . . . . . . 13 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘)) Fn 𝐡)
15482eleq2d 2813 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀) ↔ 𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž)))
155154biimpa 476 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ 𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž))
156141, 155nat1st2nd 17914 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ 𝑏 ∈ (⟨(1st β€˜((1st β€˜π‘Œ)β€˜π‘€)), (2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))⟩(𝑂 Nat 𝑆)⟨(1st β€˜β„Ž), (2nd β€˜β„Ž)⟩))
157141, 156, 7natfn 17917 . . . . . . . . . . . . 13 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ 𝑏 Fn 𝐡)
158142adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ 𝐢 ∈ Cat)
159147adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ 𝑀 ∈ 𝐡)
160 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 ∈ 𝐡)
16110, 6, 158, 159, 107, 160yon11 18229 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§) = (𝑧(Hom β€˜πΆ)𝑀))
162161eleq2d 2813 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (π‘˜ ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§) ↔ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)))
163162biimpa 476 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)) β†’ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀))
164158adantr 480 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ 𝐢 ∈ Cat)
165143ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ 𝑉 ∈ π‘Š)
166144ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ran (Homf β€˜πΆ) βŠ† π‘ˆ)
167145ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (ran (Homf β€˜π‘„) βˆͺ π‘ˆ) βŠ† 𝑉)
168146ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ β„Ž ∈ (𝑂 Func 𝑆))
169159adantr 480 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ 𝑀 ∈ 𝐡)
170150ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((β„Žπ‘€π‘€)β€˜π‘) ∈ ((1st β€˜β„Ž)β€˜π‘€))
171 simplr 766 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ 𝑧 ∈ 𝐡)
172 simpr 484 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀))
17310, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 42, 170, 171, 172yonedalem4b 18241 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§)β€˜π‘˜) = (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)β€˜((β„Žπ‘€π‘€)β€˜π‘)))
17410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 26yonedalem3a 18239 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((β„Žπ‘€π‘€) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€))) ∧ (β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢(β„Ž(1st β€˜πΈ)𝑀)))
175174simpld 494 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (β„Žπ‘€π‘€) = (π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€))))
176175fveq1d 6887 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((β„Žπ‘€π‘€)β€˜π‘) = ((π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)))β€˜π‘))
177155ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ 𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž))
178 fveq1 6884 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = 𝑏 β†’ (π‘Žβ€˜π‘€) = (π‘β€˜π‘€))
179178fveq1d 6887 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = 𝑏 β†’ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)) = ((π‘β€˜π‘€)β€˜( 1 β€˜π‘€)))
180 fvex 6898 . . . . . . . . . . . . . . . . . . . . 21 ((π‘β€˜π‘€)β€˜( 1 β€˜π‘€)) ∈ V
181179, 102, 180fvmpt 6992 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) β†’ ((π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)))β€˜π‘) = ((π‘β€˜π‘€)β€˜( 1 β€˜π‘€)))
182177, 181syl 17 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((π‘Ž ∈ (((1st β€˜π‘Œ)β€˜π‘€)(𝑂 Nat 𝑆)β„Ž) ↦ ((π‘Žβ€˜π‘€)β€˜( 1 β€˜π‘€)))β€˜π‘) = ((π‘β€˜π‘€)β€˜( 1 β€˜π‘€)))
183176, 182eqtrd 2766 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((β„Žπ‘€π‘€)β€˜π‘) = ((π‘β€˜π‘€)β€˜( 1 β€˜π‘€)))
184183fveq2d 6889 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)β€˜((β„Žπ‘€π‘€)β€˜π‘)) = (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)β€˜((π‘β€˜π‘€)β€˜( 1 β€˜π‘€))))
185156ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ 𝑏 ∈ (⟨(1st β€˜((1st β€˜π‘Œ)β€˜π‘€)), (2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))⟩(𝑂 Nat 𝑆)⟨(1st β€˜β„Ž), (2nd β€˜β„Ž)⟩))
186 eqid 2726 . . . . . . . . . . . . . . . . . . . . . 22 (Hom β€˜π‘‚) = (Hom β€˜π‘‚)
187 eqid 2726 . . . . . . . . . . . . . . . . . . . . . 22 (compβ€˜π‘†) = (compβ€˜π‘†)
188107, 5oppchom 17669 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀(Hom β€˜π‘‚)𝑧) = (𝑧(Hom β€˜πΆ)𝑀)
189172, 188eleqtrrdi 2838 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ π‘˜ ∈ (𝑀(Hom β€˜π‘‚)𝑧))
190141, 185, 7, 186, 187, 169, 171, 189nati 17918 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((π‘β€˜π‘§)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€), ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)⟩(compβ€˜π‘†)((1st β€˜β„Ž)β€˜π‘§))((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)) = (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€), ((1st β€˜β„Ž)β€˜π‘€)⟩(compβ€˜π‘†)((1st β€˜β„Ž)β€˜π‘§))(π‘β€˜π‘€)))
19177ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ π‘ˆ ∈ V)
192191adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ π‘ˆ ∈ V)
193192adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ π‘ˆ ∈ V)
194 relfunc 17821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Rel (𝐢 Func 𝑄)
19510, 17, 5, 12, 3, 77, 19yoncl 18227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (πœ‘ β†’ π‘Œ ∈ (𝐢 Func 𝑄))
196 1st2ndbr 8027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Rel (𝐢 Func 𝑄) ∧ π‘Œ ∈ (𝐢 Func 𝑄)) β†’ (1st β€˜π‘Œ)(𝐢 Func 𝑄)(2nd β€˜π‘Œ))
197194, 195, 196sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (1st β€˜π‘Œ)(𝐢 Func 𝑄)(2nd β€˜π‘Œ))
1986, 4, 197funcf1 17825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ (1st β€˜π‘Œ):𝐡⟢(𝑂 Func 𝑆))
199198ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (1st β€˜π‘Œ):𝐡⟢(𝑂 Func 𝑆))
200199, 147ffvelcdmd 7081 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((1st β€˜π‘Œ)β€˜π‘€) ∈ (𝑂 Func 𝑆))
201 1st2ndbr 8027 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel (𝑂 Func 𝑆) ∧ ((1st β€˜π‘Œ)β€˜π‘€) ∈ (𝑂 Func 𝑆)) β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘€))(𝑂 Func 𝑆)(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€)))
202112, 200, 201sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘€))(𝑂 Func 𝑆)(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€)))
2037, 121, 202funcf1 17825 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘€)):𝐡⟢(Baseβ€˜π‘†))
20412, 191setcbas 18040 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ π‘ˆ = (Baseβ€˜π‘†))
205204feq3d 6698 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€)):π΅βŸΆπ‘ˆ ↔ (1st β€˜((1st β€˜π‘Œ)β€˜π‘€)):𝐡⟢(Baseβ€˜π‘†)))
206203, 205mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘€)):π΅βŸΆπ‘ˆ)
207206, 147ffvelcdmd 7081 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€) ∈ π‘ˆ)
208207ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€) ∈ π‘ˆ)
209206ffvelcdmda 7080 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§) ∈ π‘ˆ)
210209adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§) ∈ π‘ˆ)
211112, 146, 113sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (1st β€˜β„Ž)(𝑂 Func 𝑆)(2nd β€˜β„Ž))
2127, 121, 211funcf1 17825 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (1st β€˜β„Ž):𝐡⟢(Baseβ€˜π‘†))
213204feq3d 6698 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((1st β€˜β„Ž):π΅βŸΆπ‘ˆ ↔ (1st β€˜β„Ž):𝐡⟢(Baseβ€˜π‘†)))
214212, 213mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (1st β€˜β„Ž):π΅βŸΆπ‘ˆ)
215214ffvelcdmda 7080 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ ((1st β€˜β„Ž)β€˜π‘§) ∈ π‘ˆ)
216215adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((1st β€˜β„Ž)β€˜π‘§) ∈ π‘ˆ)
217 eqid 2726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Hom β€˜π‘†) = (Hom β€˜π‘†)
218202ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (1st β€˜((1st β€˜π‘Œ)β€˜π‘€))(𝑂 Func 𝑆)(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€)))
2197, 186, 217, 218, 169, 171funcf2 17827 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧):(𝑀(Hom β€˜π‘‚)𝑧)⟢(((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)(Hom β€˜π‘†)((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)))
220219, 189ffvelcdmd 7081 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)(Hom β€˜π‘†)((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)))
22112, 193, 217, 208, 210elsetchom 18043 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)(Hom β€˜π‘†)((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)) ↔ ((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)))
222220, 221mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)⟢((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§))
223156adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ 𝑏 ∈ (⟨(1st β€˜((1st β€˜π‘Œ)β€˜π‘€)), (2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))⟩(𝑂 Nat 𝑆)⟨(1st β€˜β„Ž), (2nd β€˜β„Ž)⟩))
224141, 223, 7, 217, 160natcl 17916 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (π‘β€˜π‘§) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘§)))
22512, 192, 217, 209, 215elsetchom 18043 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ ((π‘β€˜π‘§) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘§)) ↔ (π‘β€˜π‘§):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)⟢((1st β€˜β„Ž)β€˜π‘§)))
226224, 225mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (π‘β€˜π‘§):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)⟢((1st β€˜β„Ž)β€˜π‘§))
227226adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (π‘β€˜π‘§):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)⟢((1st β€˜β„Ž)β€˜π‘§))
22812, 193, 187, 208, 210, 216, 222, 227setcco 18045 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((π‘β€˜π‘§)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€), ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)⟩(compβ€˜π‘†)((1st β€˜β„Ž)β€˜π‘§))((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)) = ((π‘β€˜π‘§) ∘ ((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)))
229214, 147ffvelcdmd 7081 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((1st β€˜β„Ž)β€˜π‘€) ∈ π‘ˆ)
230229ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((1st β€˜β„Ž)β€˜π‘€) ∈ π‘ˆ)
231141, 156, 7, 217, 147natcl 17916 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (π‘β€˜π‘€) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘€)))
23212, 191, 217, 207, 229elsetchom 18043 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((π‘β€˜π‘€) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘€)) ↔ (π‘β€˜π‘€):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)⟢((1st β€˜β„Ž)β€˜π‘€)))
233231, 232mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ (π‘β€˜π‘€):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)⟢((1st β€˜β„Ž)β€˜π‘€))
234233ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (π‘β€˜π‘€):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€)⟢((1st β€˜β„Ž)β€˜π‘€))
235112, 168, 113sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (1st β€˜β„Ž)(𝑂 Func 𝑆)(2nd β€˜β„Ž))
2367, 186, 217, 235, 169, 171funcf2 17827 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (𝑀(2nd β€˜β„Ž)𝑧):(𝑀(Hom β€˜π‘‚)𝑧)⟢(((1st β€˜β„Ž)β€˜π‘€)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘§)))
237236, 189ffvelcdmd 7081 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜) ∈ (((1st β€˜β„Ž)β€˜π‘€)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘§)))
23812, 193, 217, 230, 216elsetchom 18043 . . . . . . . . . . . . . . . . . . . . . . 23 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜) ∈ (((1st β€˜β„Ž)β€˜π‘€)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘§)) ↔ ((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜):((1st β€˜β„Ž)β€˜π‘€)⟢((1st β€˜β„Ž)β€˜π‘§)))
239237, 238mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜):((1st β€˜β„Ž)β€˜π‘€)⟢((1st β€˜β„Ž)β€˜π‘§))
24012, 193, 187, 208, 230, 216, 234, 239setcco 18045 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)(⟨((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€), ((1st β€˜β„Ž)β€˜π‘€)⟩(compβ€˜π‘†)((1st β€˜β„Ž)β€˜π‘§))(π‘β€˜π‘€)) = (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜) ∘ (π‘β€˜π‘€)))
241190, 228, 2403eqtr3d 2774 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((π‘β€˜π‘§) ∘ ((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)) = (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜) ∘ (π‘β€˜π‘€)))
242241fveq1d 6887 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((π‘β€˜π‘§) ∘ ((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜))β€˜( 1 β€˜π‘€)) = ((((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜) ∘ (π‘β€˜π‘€))β€˜( 1 β€˜π‘€)))
2436, 107, 11, 142, 147catidcl 17635 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ( 1 β€˜π‘€) ∈ (𝑀(Hom β€˜πΆ)𝑀))
24410, 6, 142, 147, 107, 147yon11 18229 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€) = (𝑀(Hom β€˜πΆ)𝑀))
245243, 244eleqtrrd 2830 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ( 1 β€˜π‘€) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€))
246245ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ( 1 β€˜π‘€) ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘€))
247222, 246fvco3d 6985 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((π‘β€˜π‘§) ∘ ((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜))β€˜( 1 β€˜π‘€)) = ((π‘β€˜π‘§)β€˜(((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)β€˜( 1 β€˜π‘€))))
248233, 245fvco3d 6985 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜) ∘ (π‘β€˜π‘€))β€˜( 1 β€˜π‘€)) = (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)β€˜((π‘β€˜π‘€)β€˜( 1 β€˜π‘€))))
249248ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜) ∘ (π‘β€˜π‘€))β€˜( 1 β€˜π‘€)) = (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)β€˜((π‘β€˜π‘€)β€˜( 1 β€˜π‘€))))
250242, 247, 2493eqtr3d 2774 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((π‘β€˜π‘§)β€˜(((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)β€˜( 1 β€˜π‘€))) = (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)β€˜((π‘β€˜π‘€)β€˜( 1 β€˜π‘€))))
251 eqid 2726 . . . . . . . . . . . . . . . . . . . . 21 (compβ€˜πΆ) = (compβ€˜πΆ)
252243ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ( 1 β€˜π‘€) ∈ (𝑀(Hom β€˜πΆ)𝑀))
25310, 6, 164, 169, 107, 169, 251, 171, 172, 252yon12 18230 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)β€˜( 1 β€˜π‘€)) = (( 1 β€˜π‘€)(βŸ¨π‘§, π‘€βŸ©(compβ€˜πΆ)𝑀)π‘˜))
2546, 107, 11, 164, 171, 251, 169, 172catlid 17636 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (( 1 β€˜π‘€)(βŸ¨π‘§, π‘€βŸ©(compβ€˜πΆ)𝑀)π‘˜) = π‘˜)
255253, 254eqtrd 2766 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)β€˜( 1 β€˜π‘€)) = π‘˜)
256255fveq2d 6889 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((π‘β€˜π‘§)β€˜(((𝑀(2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))𝑧)β€˜π‘˜)β€˜( 1 β€˜π‘€))) = ((π‘β€˜π‘§)β€˜π‘˜))
257250, 256eqtr3d 2768 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ (((𝑀(2nd β€˜β„Ž)𝑧)β€˜π‘˜)β€˜((π‘β€˜π‘€)β€˜( 1 β€˜π‘€))) = ((π‘β€˜π‘§)β€˜π‘˜))
258173, 184, 2573eqtrd 2770 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ (𝑧(Hom β€˜πΆ)𝑀)) β†’ ((((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§)β€˜π‘˜) = ((π‘β€˜π‘§)β€˜π‘˜))
259163, 258syldan 590 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) ∧ π‘˜ ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)) β†’ ((((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§)β€˜π‘˜) = ((π‘β€˜π‘§)β€˜π‘˜))
260259mpteq2dva 5241 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (π‘˜ ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§) ↦ ((((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§)β€˜π‘˜)) = (π‘˜ ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§) ↦ ((π‘β€˜π‘§)β€˜π‘˜)))
261152adantr 480 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘)) ∈ (⟨(1st β€˜((1st β€˜π‘Œ)β€˜π‘€)), (2nd β€˜((1st β€˜π‘Œ)β€˜π‘€))⟩(𝑂 Nat 𝑆)⟨(1st β€˜β„Ž), (2nd β€˜β„Ž)⟩))
262141, 261, 7, 217, 160natcl 17916 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘§)))
26312, 192, 217, 209, 215elsetchom 18043 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ ((((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§) ∈ (((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)(Hom β€˜π‘†)((1st β€˜β„Ž)β€˜π‘§)) ↔ (((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)⟢((1st β€˜β„Ž)β€˜π‘§)))
264262, 263mpbid 231 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§):((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§)⟢((1st β€˜β„Ž)β€˜π‘§))
265264feqmptd 6954 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§) = (π‘˜ ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§) ↦ ((((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§)β€˜π‘˜)))
266226feqmptd 6954 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (π‘β€˜π‘§) = (π‘˜ ∈ ((1st β€˜((1st β€˜π‘Œ)β€˜π‘€))β€˜π‘§) ↦ ((π‘β€˜π‘§)β€˜π‘˜)))
267260, 265, 2663eqtr4d 2776 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) ∧ 𝑧 ∈ 𝐡) β†’ (((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))β€˜π‘§) = (π‘β€˜π‘§))
268153, 157, 267eqfnfvd 7029 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) ∧ 𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀)) β†’ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘)) = 𝑏)
269268mpteq2dva 5241 . . . . . . . . . . 11 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀) ↦ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))) = (𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀) ↦ 𝑏))
270 mptresid 6044 . . . . . . . . . . 11 ( I β†Ύ (β„Ž(1st β€˜π‘)𝑀)) = (𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀) ↦ 𝑏)
271269, 270eqtr4di 2784 . . . . . . . . . 10 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (𝑏 ∈ (β„Ž(1st β€˜π‘)𝑀) ↦ ((β„Žπ‘π‘€)β€˜((β„Žπ‘€π‘€)β€˜π‘))) = ( I β†Ύ (β„Ž(1st β€˜π‘)𝑀)))
272140, 271eqtrd 2766 . . . . . . . . 9 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘π‘€) ∘ (β„Žπ‘€π‘€)) = ( I β†Ύ (β„Ž(1st β€˜π‘)𝑀)))
273 fcof1o 7290 . . . . . . . . 9 ((((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)⟢(β„Ž(1st β€˜πΈ)𝑀) ∧ (β„Žπ‘π‘€):(β„Ž(1st β€˜πΈ)𝑀)⟢(β„Ž(1st β€˜π‘)𝑀)) ∧ (((β„Žπ‘€π‘€) ∘ (β„Žπ‘π‘€)) = ( I β†Ύ (β„Ž(1st β€˜πΈ)𝑀)) ∧ ((β„Žπ‘π‘€) ∘ (β„Žπ‘€π‘€)) = ( I β†Ύ (β„Ž(1st β€˜π‘)𝑀)))) β†’ ((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)–1-1-ontoβ†’(β„Ž(1st β€˜πΈ)𝑀) ∧ β—‘(β„Žπ‘€π‘€) = (β„Žπ‘π‘€)))
27435, 84, 138, 272, 273syl22anc 836 . . . . . . . 8 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)–1-1-ontoβ†’(β„Ž(1st β€˜πΈ)𝑀) ∧ β—‘(β„Žπ‘€π‘€) = (β„Žπ‘π‘€)))
275 eqcom 2733 . . . . . . . . 9 (β—‘(β„Žπ‘€π‘€) = (β„Žπ‘π‘€) ↔ (β„Žπ‘π‘€) = β—‘(β„Žπ‘€π‘€))
276275anbi2i 622 . . . . . . . 8 (((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)–1-1-ontoβ†’(β„Ž(1st β€˜πΈ)𝑀) ∧ β—‘(β„Žπ‘€π‘€) = (β„Žπ‘π‘€)) ↔ ((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)–1-1-ontoβ†’(β„Ž(1st β€˜πΈ)𝑀) ∧ (β„Žπ‘π‘€) = β—‘(β„Žπ‘€π‘€)))
277274, 276sylib 217 . . . . . . 7 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)–1-1-ontoβ†’(β„Ž(1st β€˜πΈ)𝑀) ∧ (β„Žπ‘π‘€) = β—‘(β„Žπ‘€π‘€)))
278 eqid 2726 . . . . . . . . . . 11 (Baseβ€˜π‘‡) = (Baseβ€˜π‘‡)
279 relfunc 17821 . . . . . . . . . . . 12 Rel ((𝑄 Γ—c 𝑂) Func 𝑇)
280 1st2ndbr 8027 . . . . . . . . . . . 12 ((Rel ((𝑄 Γ—c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇)) β†’ (1st β€˜π‘)((𝑄 Γ—c 𝑂) Func 𝑇)(2nd β€˜π‘))
281279, 22, 280sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ (1st β€˜π‘)((𝑄 Γ—c 𝑂) Func 𝑇)(2nd β€˜π‘))
2828, 278, 281funcf1 17825 . . . . . . . . . 10 (πœ‘ β†’ (1st β€˜π‘):((𝑂 Func 𝑆) Γ— 𝐡)⟢(Baseβ€˜π‘‡))
28313, 18setcbas 18040 . . . . . . . . . . 11 (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘‡))
284283feq3d 6698 . . . . . . . . . 10 (πœ‘ β†’ ((1st β€˜π‘):((𝑂 Func 𝑆) Γ— 𝐡)βŸΆπ‘‰ ↔ (1st β€˜π‘):((𝑂 Func 𝑆) Γ— 𝐡)⟢(Baseβ€˜π‘‡)))
285282, 284mpbird 257 . . . . . . . . 9 (πœ‘ β†’ (1st β€˜π‘):((𝑂 Func 𝑆) Γ— 𝐡)βŸΆπ‘‰)
286285fovcdmda 7575 . . . . . . . 8 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Ž(1st β€˜π‘)𝑀) ∈ 𝑉)
287 1st2ndbr 8027 . . . . . . . . . . . 12 ((Rel ((𝑄 Γ—c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 Γ—c 𝑂) Func 𝑇)) β†’ (1st β€˜πΈ)((𝑄 Γ—c 𝑂) Func 𝑇)(2nd β€˜πΈ))
288279, 23, 287sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ (1st β€˜πΈ)((𝑄 Γ—c 𝑂) Func 𝑇)(2nd β€˜πΈ))
2898, 278, 288funcf1 17825 . . . . . . . . . 10 (πœ‘ β†’ (1st β€˜πΈ):((𝑂 Func 𝑆) Γ— 𝐡)⟢(Baseβ€˜π‘‡))
290283feq3d 6698 . . . . . . . . . 10 (πœ‘ β†’ ((1st β€˜πΈ):((𝑂 Func 𝑆) Γ— 𝐡)βŸΆπ‘‰ ↔ (1st β€˜πΈ):((𝑂 Func 𝑆) Γ— 𝐡)⟢(Baseβ€˜π‘‡)))
291289, 290mpbird 257 . . . . . . . . 9 (πœ‘ β†’ (1st β€˜πΈ):((𝑂 Func 𝑆) Γ— 𝐡)βŸΆπ‘‰)
292291fovcdmda 7575 . . . . . . . 8 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Ž(1st β€˜πΈ)𝑀) ∈ 𝑉)
29313, 29, 286, 292, 25setcinv 18052 . . . . . . 7 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ ((β„Žπ‘€π‘€)((β„Ž(1st β€˜π‘)𝑀)(Invβ€˜π‘‡)(β„Ž(1st β€˜πΈ)𝑀))(β„Žπ‘π‘€) ↔ ((β„Žπ‘€π‘€):(β„Ž(1st β€˜π‘)𝑀)–1-1-ontoβ†’(β„Ž(1st β€˜πΈ)𝑀) ∧ (β„Žπ‘π‘€) = β—‘(β„Žπ‘€π‘€))))
294277, 293mpbird 257 . . . . . 6 ((πœ‘ ∧ (β„Ž ∈ (𝑂 Func 𝑆) ∧ 𝑀 ∈ 𝐡)) β†’ (β„Žπ‘€π‘€)((β„Ž(1st β€˜π‘)𝑀)(Invβ€˜π‘‡)(β„Ž(1st β€˜πΈ)𝑀))(β„Žπ‘π‘€))
295294ralrimivva 3194 . . . . 5 (πœ‘ β†’ βˆ€β„Ž ∈ (𝑂 Func 𝑆)βˆ€π‘€ ∈ 𝐡 (β„Žπ‘€π‘€)((β„Ž(1st β€˜π‘)𝑀)(Invβ€˜π‘‡)(β„Ž(1st β€˜πΈ)𝑀))(β„Žπ‘π‘€))
296 fveq2 6885 . . . . . . . 8 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ (π‘€β€˜π‘§) = (π‘€β€˜βŸ¨β„Ž, π‘€βŸ©))
297 df-ov 7408 . . . . . . . 8 (β„Žπ‘€π‘€) = (π‘€β€˜βŸ¨β„Ž, π‘€βŸ©)
298296, 297eqtr4di 2784 . . . . . . 7 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ (π‘€β€˜π‘§) = (β„Žπ‘€π‘€))
299 fveq2 6885 . . . . . . . . 9 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ ((1st β€˜π‘)β€˜π‘§) = ((1st β€˜π‘)β€˜βŸ¨β„Ž, π‘€βŸ©))
300 df-ov 7408 . . . . . . . . 9 (β„Ž(1st β€˜π‘)𝑀) = ((1st β€˜π‘)β€˜βŸ¨β„Ž, π‘€βŸ©)
301299, 300eqtr4di 2784 . . . . . . . 8 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ ((1st β€˜π‘)β€˜π‘§) = (β„Ž(1st β€˜π‘)𝑀))
302 fveq2 6885 . . . . . . . . 9 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ ((1st β€˜πΈ)β€˜π‘§) = ((1st β€˜πΈ)β€˜βŸ¨β„Ž, π‘€βŸ©))
303 df-ov 7408 . . . . . . . . 9 (β„Ž(1st β€˜πΈ)𝑀) = ((1st β€˜πΈ)β€˜βŸ¨β„Ž, π‘€βŸ©)
304302, 303eqtr4di 2784 . . . . . . . 8 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ ((1st β€˜πΈ)β€˜π‘§) = (β„Ž(1st β€˜πΈ)𝑀))
305301, 304oveq12d 7423 . . . . . . 7 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ (((1st β€˜π‘)β€˜π‘§)(Invβ€˜π‘‡)((1st β€˜πΈ)β€˜π‘§)) = ((β„Ž(1st β€˜π‘)𝑀)(Invβ€˜π‘‡)(β„Ž(1st β€˜πΈ)𝑀)))
306 fveq2 6885 . . . . . . . 8 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ (π‘β€˜π‘§) = (π‘β€˜βŸ¨β„Ž, π‘€βŸ©))
307 df-ov 7408 . . . . . . . 8 (β„Žπ‘π‘€) = (π‘β€˜βŸ¨β„Ž, π‘€βŸ©)
308306, 307eqtr4di 2784 . . . . . . 7 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ (π‘β€˜π‘§) = (β„Žπ‘π‘€))
309298, 305, 308breq123d 5155 . . . . . 6 (𝑧 = βŸ¨β„Ž, π‘€βŸ© β†’ ((π‘€β€˜π‘§)(((1st β€˜π‘)β€˜π‘§)(Invβ€˜π‘‡)((1st β€˜πΈ)β€˜π‘§))(π‘β€˜π‘§) ↔ (β„Žπ‘€π‘€)((β„Ž(1st β€˜π‘)𝑀)(Invβ€˜π‘‡)(β„Ž(1st β€˜πΈ)𝑀))(β„Žπ‘π‘€)))
310309ralxp 5835 . . . . 5 (βˆ€π‘§ ∈ ((𝑂 Func 𝑆) Γ— 𝐡)(π‘€β€˜π‘§)(((1st β€˜π‘)β€˜π‘§)(Invβ€˜π‘‡)((1st β€˜πΈ)β€˜π‘§))(π‘β€˜π‘§) ↔ βˆ€β„Ž ∈ (𝑂 Func 𝑆)βˆ€π‘€ ∈ 𝐡 (β„Žπ‘€π‘€)((β„Ž(1st β€˜π‘)𝑀)(Invβ€˜π‘‡)(β„Ž(1st β€˜πΈ)𝑀))(β„Žπ‘π‘€))
311295, 310sylibr 233 . . . 4 (πœ‘ β†’ βˆ€π‘§ ∈ ((𝑂 Func 𝑆) Γ— 𝐡)(π‘€β€˜π‘§)(((1st β€˜π‘)β€˜π‘§)(Invβ€˜π‘‡)((1st β€˜πΈ)β€˜π‘§))(π‘β€˜π‘§))
312311r19.21bi 3242 . . 3 ((πœ‘ ∧ 𝑧 ∈ ((𝑂 Func 𝑆) Γ— 𝐡)) β†’ (π‘€β€˜π‘§)(((1st β€˜π‘)β€˜π‘§)(Invβ€˜π‘‡)((1st β€˜πΈ)β€˜π‘§))(π‘β€˜π‘§))
3131, 8, 9, 22, 23, 24, 25, 27, 312invfuc 17939 . 2 (πœ‘ β†’ 𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) Γ— 𝐡) ↦ (π‘β€˜π‘§)))
314 fvex 6898 . . . . 5 ((1st β€˜π‘“)β€˜π‘₯) ∈ V
315314mptex 7220 . . . 4 (𝑒 ∈ ((1st β€˜π‘“)β€˜π‘₯) ↦ (𝑦 ∈ 𝐡 ↦ (𝑔 ∈ (𝑦(Hom β€˜πΆ)π‘₯) ↦ (((π‘₯(2nd β€˜π‘“)𝑦)β€˜π‘”)β€˜π‘’)))) ∈ V
31642, 315fnmpoi 8055 . . 3 𝑁 Fn ((𝑂 Func 𝑆) Γ— 𝐡)
317 dffn5 6944 . . 3 (𝑁 Fn ((𝑂 Func 𝑆) Γ— 𝐡) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) Γ— 𝐡) ↦ (π‘β€˜π‘§)))
318316, 317mpbi 229 . 2 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) Γ— 𝐡) ↦ (π‘β€˜π‘§))
319313, 318breqtrrdi 5183 1 (πœ‘ β†’ 𝑀(𝑍𝐼𝐸)𝑁)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  Vcvv 3468   βˆͺ cun 3941   βŠ† wss 3943  βŸ¨cop 4629   class class class wbr 5141   ↦ cmpt 5224   I cid 5566   Γ— cxp 5667  β—‘ccnv 5668  ran crn 5670   β†Ύ cres 5671   ∘ ccom 5673  Rel wrel 5674   Fn wfn 6532  βŸΆwf 6533  β€“1-1-ontoβ†’wf1o 6536  β€˜cfv 6537  (class class class)co 7405   ∈ cmpo 7407  1st c1st 7972  2nd c2nd 7973  tpos ctpos 8211  Basecbs 17153  Hom chom 17217  compcco 17218  Catccat 17617  Idccid 17618  Homf chomf 17619  oppCatcoppc 17664  Invcinv 17701   Func cfunc 17813   ∘func ccofu 17815   Nat cnat 17904   FuncCat cfuc 17905  SetCatcsetc 18037   Γ—c cxpc 18132   1stF c1stf 18133   2ndF c2ndf 18134   ⟨,⟩F cprf 18135   evalF cevlf 18174  HomFchof 18213  Yoncyon 18214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-tpos 8212  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-fz 13491  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-hom 17230  df-cco 17231  df-cat 17621  df-cid 17622  df-homf 17623  df-comf 17624  df-oppc 17665  df-sect 17703  df-inv 17704  df-ssc 17766  df-resc 17767  df-subc 17768  df-func 17817  df-cofu 17819  df-nat 17906  df-fuc 17907  df-setc 18038  df-xpc 18136  df-1stf 18137  df-2ndf 18138  df-prf 18139  df-evlf 18178  df-curf 18179  df-hof 18215  df-yon 18216
This theorem is referenced by:  yonffthlem  18247  yoneda  18248
  Copyright terms: Public domain W3C validator