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

Theorem catcfuccl 18074
Description: The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 14-Oct-2024.)
Hypotheses
Ref Expression
catcfuccl.c 𝐢 = (CatCatβ€˜π‘ˆ)
catcfuccl.b 𝐡 = (Baseβ€˜πΆ)
catcfuccl.o 𝑄 = (𝑋 FuncCat π‘Œ)
catcfuccl.u (πœ‘ β†’ π‘ˆ ∈ WUni)
catcfuccl.1 (πœ‘ β†’ Ο‰ ∈ π‘ˆ)
catcfuccl.x (πœ‘ β†’ 𝑋 ∈ 𝐡)
catcfuccl.y (πœ‘ β†’ π‘Œ ∈ 𝐡)
Assertion
Ref Expression
catcfuccl (πœ‘ β†’ 𝑄 ∈ 𝐡)

Proof of Theorem catcfuccl
Dummy variables π‘Ž 𝑏 𝑓 𝑔 β„Ž 𝑣 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcfuccl.o . . . . 5 𝑄 = (𝑋 FuncCat π‘Œ)
2 eqid 2731 . . . . 5 (𝑋 Func π‘Œ) = (𝑋 Func π‘Œ)
3 eqid 2731 . . . . 5 (𝑋 Nat π‘Œ) = (𝑋 Nat π‘Œ)
4 eqid 2731 . . . . 5 (Baseβ€˜π‘‹) = (Baseβ€˜π‘‹)
5 eqid 2731 . . . . 5 (compβ€˜π‘Œ) = (compβ€˜π‘Œ)
6 catcfuccl.x . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ 𝐡)
7 catcfuccl.c . . . . . . . 8 𝐢 = (CatCatβ€˜π‘ˆ)
8 catcfuccl.b . . . . . . . 8 𝐡 = (Baseβ€˜πΆ)
9 catcfuccl.u . . . . . . . 8 (πœ‘ β†’ π‘ˆ ∈ WUni)
107, 8, 9catcbas 18056 . . . . . . 7 (πœ‘ β†’ 𝐡 = (π‘ˆ ∩ Cat))
116, 10eleqtrd 2834 . . . . . 6 (πœ‘ β†’ 𝑋 ∈ (π‘ˆ ∩ Cat))
1211elin2d 4200 . . . . 5 (πœ‘ β†’ 𝑋 ∈ Cat)
13 catcfuccl.y . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ 𝐡)
1413, 10eleqtrd 2834 . . . . . 6 (πœ‘ β†’ π‘Œ ∈ (π‘ˆ ∩ Cat))
1514elin2d 4200 . . . . 5 (πœ‘ β†’ π‘Œ ∈ Cat)
16 eqidd 2732 . . . . 5 (πœ‘ β†’ (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))) = (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))))
171, 2, 3, 4, 5, 12, 15, 16fucval 17915 . . . 4 (πœ‘ β†’ 𝑄 = {⟨(Baseβ€˜ndx), (𝑋 Func π‘Œ)⟩, ⟨(Hom β€˜ndx), (𝑋 Nat π‘Œ)⟩, ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩})
18 baseid 17152 . . . . . . 7 Base = Slot (Baseβ€˜ndx)
19 catcfuccl.1 . . . . . . . 8 (πœ‘ β†’ Ο‰ ∈ π‘ˆ)
209, 19wunndx 17133 . . . . . . 7 (πœ‘ β†’ ndx ∈ π‘ˆ)
2118, 9, 20wunstr 17126 . . . . . 6 (πœ‘ β†’ (Baseβ€˜ndx) ∈ π‘ˆ)
227, 8, 9, 6catcbascl 18067 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ π‘ˆ)
237, 8, 9, 13catcbascl 18067 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ π‘ˆ)
249, 22, 23wunfunc 17854 . . . . . 6 (πœ‘ β†’ (𝑋 Func π‘Œ) ∈ π‘ˆ)
259, 21, 24wunop 10720 . . . . 5 (πœ‘ β†’ ⟨(Baseβ€˜ndx), (𝑋 Func π‘Œ)⟩ ∈ π‘ˆ)
26 homid 17362 . . . . . . 7 Hom = Slot (Hom β€˜ndx)
2726, 9, 20wunstr 17126 . . . . . 6 (πœ‘ β†’ (Hom β€˜ndx) ∈ π‘ˆ)
289, 22, 23wunnat 17912 . . . . . 6 (πœ‘ β†’ (𝑋 Nat π‘Œ) ∈ π‘ˆ)
299, 27, 28wunop 10720 . . . . 5 (πœ‘ β†’ ⟨(Hom β€˜ndx), (𝑋 Nat π‘Œ)⟩ ∈ π‘ˆ)
30 ccoid 17364 . . . . . . 7 comp = Slot (compβ€˜ndx)
3130, 9, 20wunstr 17126 . . . . . 6 (πœ‘ β†’ (compβ€˜ndx) ∈ π‘ˆ)
329, 24, 24wunxp 10722 . . . . . . . 8 (πœ‘ β†’ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)) ∈ π‘ˆ)
339, 32, 24wunxp 10722 . . . . . . 7 (πœ‘ β†’ (((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)) Γ— (𝑋 Func π‘Œ)) ∈ π‘ˆ)
347, 8, 9, 13catcccocl 18071 . . . . . . . . . . . . . 14 (πœ‘ β†’ (compβ€˜π‘Œ) ∈ π‘ˆ)
359, 34wunrn 10727 . . . . . . . . . . . . 13 (πœ‘ β†’ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
369, 35wununi 10704 . . . . . . . . . . . 12 (πœ‘ β†’ βˆͺ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
379, 36wunrn 10727 . . . . . . . . . . 11 (πœ‘ β†’ ran βˆͺ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
389, 37wununi 10704 . . . . . . . . . 10 (πœ‘ β†’ βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
399, 38wunpw 10705 . . . . . . . . 9 (πœ‘ β†’ 𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
407, 8, 9, 6catcbaselcl 18069 . . . . . . . . 9 (πœ‘ β†’ (Baseβ€˜π‘‹) ∈ π‘ˆ)
419, 39, 40wunmap 10724 . . . . . . . 8 (πœ‘ β†’ (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ∈ π‘ˆ)
429, 28wunrn 10727 . . . . . . . . . 10 (πœ‘ β†’ ran (𝑋 Nat π‘Œ) ∈ π‘ˆ)
439, 42wununi 10704 . . . . . . . . 9 (πœ‘ β†’ βˆͺ ran (𝑋 Nat π‘Œ) ∈ π‘ˆ)
449, 43, 43wunxp 10722 . . . . . . . 8 (πœ‘ β†’ (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)) ∈ π‘ˆ)
459, 41, 44wunpm 10723 . . . . . . 7 (πœ‘ β†’ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))) ∈ π‘ˆ)
46 fvex 6905 . . . . . . . . . . 11 (1st β€˜π‘£) ∈ V
47 fvex 6905 . . . . . . . . . . . . . 14 (2nd β€˜π‘£) ∈ V
48 ovex 7445 . . . . . . . . . . . . . . . . 17 (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ∈ V
49 ovex 7445 . . . . . . . . . . . . . . . . . . . 20 (𝑋 Nat π‘Œ) ∈ V
5049rnex 7906 . . . . . . . . . . . . . . . . . . 19 ran (𝑋 Nat π‘Œ) ∈ V
5150uniex 7734 . . . . . . . . . . . . . . . . . 18 βˆͺ ran (𝑋 Nat π‘Œ) ∈ V
5251, 51xpex 7743 . . . . . . . . . . . . . . . . 17 (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)) ∈ V
53 eqid 2731 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))) = (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))
54 ovssunirn 7448 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) βŠ† βˆͺ ran (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))
55 ovssunirn 7448 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† βˆͺ ran (compβ€˜π‘Œ)
56 rnss 5939 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† βˆͺ ran (compβ€˜π‘Œ) β†’ ran (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† ran βˆͺ ran (compβ€˜π‘Œ))
57 uniss 4917 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† ran βˆͺ ran (compβ€˜π‘Œ) β†’ βˆͺ ran (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† βˆͺ ran βˆͺ ran (compβ€˜π‘Œ))
5855, 56, 57mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 βˆͺ ran (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† βˆͺ ran βˆͺ ran (compβ€˜π‘Œ)
5954, 58sstri 3992 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) βŠ† βˆͺ ran βˆͺ ran (compβ€˜π‘Œ)
60 ovex 7445 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) ∈ V
6160elpw 4607 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) ∈ 𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↔ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) βŠ† βˆͺ ran βˆͺ ran (compβ€˜π‘Œ))
6259, 61mpbir 230 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) ∈ 𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ)
6362a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (Baseβ€˜π‘‹) β†’ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) ∈ 𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ))
6453, 63fmpti 7114 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))):(Baseβ€˜π‘‹)βŸΆπ’« βˆͺ ran βˆͺ ran (compβ€˜π‘Œ)
65 fvex 6905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (compβ€˜π‘Œ) ∈ V
6665rnex 7906 . . . . . . . . . . . . . . . . . . . . . . . . 25 ran (compβ€˜π‘Œ) ∈ V
6766uniex 7734 . . . . . . . . . . . . . . . . . . . . . . . 24 βˆͺ ran (compβ€˜π‘Œ) ∈ V
6867rnex 7906 . . . . . . . . . . . . . . . . . . . . . . 23 ran βˆͺ ran (compβ€˜π‘Œ) ∈ V
6968uniex 7734 . . . . . . . . . . . . . . . . . . . . . 22 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ∈ V
7069pwex 5379 . . . . . . . . . . . . . . . . . . . . 21 𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ∈ V
71 fvex 6905 . . . . . . . . . . . . . . . . . . . . 21 (Baseβ€˜π‘‹) ∈ V
7270, 71elmap 8868 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))) ∈ (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↔ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))):(Baseβ€˜π‘‹)βŸΆπ’« βˆͺ ran βˆͺ ran (compβ€˜π‘Œ))
7364, 72mpbir 230 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))) ∈ (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹))
7473rgen2w 3065 . . . . . . . . . . . . . . . . . 18 βˆ€π‘ ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž)βˆ€π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔)(π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))) ∈ (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹))
75 eqid 2731 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) = (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))
7675fmpo 8057 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘ ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž)βˆ€π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔)(π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))) ∈ (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↔ (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))):((𝑔(𝑋 Nat π‘Œ)β„Ž) Γ— (𝑓(𝑋 Nat π‘Œ)𝑔))⟢(𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)))
7774, 76mpbi 229 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))):((𝑔(𝑋 Nat π‘Œ)β„Ž) Γ— (𝑓(𝑋 Nat π‘Œ)𝑔))⟢(𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹))
78 ovssunirn 7448 . . . . . . . . . . . . . . . . . 18 (𝑔(𝑋 Nat π‘Œ)β„Ž) βŠ† βˆͺ ran (𝑋 Nat π‘Œ)
79 ovssunirn 7448 . . . . . . . . . . . . . . . . . 18 (𝑓(𝑋 Nat π‘Œ)𝑔) βŠ† βˆͺ ran (𝑋 Nat π‘Œ)
80 xpss12 5692 . . . . . . . . . . . . . . . . . 18 (((𝑔(𝑋 Nat π‘Œ)β„Ž) βŠ† βˆͺ ran (𝑋 Nat π‘Œ) ∧ (𝑓(𝑋 Nat π‘Œ)𝑔) βŠ† βˆͺ ran (𝑋 Nat π‘Œ)) β†’ ((𝑔(𝑋 Nat π‘Œ)β„Ž) Γ— (𝑓(𝑋 Nat π‘Œ)𝑔)) βŠ† (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))
8178, 79, 80mp2an 689 . . . . . . . . . . . . . . . . 17 ((𝑔(𝑋 Nat π‘Œ)β„Ž) Γ— (𝑓(𝑋 Nat π‘Œ)𝑔)) βŠ† (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))
82 elpm2r 8842 . . . . . . . . . . . . . . . . 17 ((((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ∈ V ∧ (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)) ∈ V) ∧ ((𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))):((𝑔(𝑋 Nat π‘Œ)β„Ž) Γ— (𝑓(𝑋 Nat π‘Œ)𝑔))⟢(𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ∧ ((𝑔(𝑋 Nat π‘Œ)β„Ž) Γ— (𝑓(𝑋 Nat π‘Œ)𝑔)) βŠ† (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))) β†’ (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
8348, 52, 77, 81, 82mp4an 690 . . . . . . . . . . . . . . . 16 (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))
8483sbcth 3793 . . . . . . . . . . . . . . 15 ((2nd β€˜π‘£) ∈ V β†’ [(2nd β€˜π‘£) / 𝑔](𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
85 sbcel1g 4414 . . . . . . . . . . . . . . 15 ((2nd β€˜π‘£) ∈ V β†’ ([(2nd β€˜π‘£) / 𝑔](𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))) ↔ ⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))))
8684, 85mpbid 231 . . . . . . . . . . . . . 14 ((2nd β€˜π‘£) ∈ V β†’ ⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
8747, 86ax-mp 5 . . . . . . . . . . . . 13 ⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))
8887sbcth 3793 . . . . . . . . . . . 12 ((1st β€˜π‘£) ∈ V β†’ [(1st β€˜π‘£) / 𝑓]⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
89 sbcel1g 4414 . . . . . . . . . . . 12 ((1st β€˜π‘£) ∈ V β†’ ([(1st β€˜π‘£) / 𝑓]⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))) ↔ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))))
9088, 89mpbid 231 . . . . . . . . . . 11 ((1st β€˜π‘£) ∈ V β†’ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
9146, 90ax-mp 5 . . . . . . . . . 10 ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))
9291rgen2w 3065 . . . . . . . . 9 βˆ€π‘£ ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ))βˆ€β„Ž ∈ (𝑋 Func π‘Œ)⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))
93 eqid 2731 . . . . . . . . . 10 (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))) = (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))
9493fmpo 8057 . . . . . . . . 9 (βˆ€π‘£ ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ))βˆ€β„Ž ∈ (𝑋 Func π‘Œ)⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))) ↔ (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))):(((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)) Γ— (𝑋 Func π‘Œ))⟢((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
9592, 94mpbi 229 . . . . . . . 8 (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))):(((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)) Γ— (𝑋 Func π‘Œ))⟢((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))
9695a1i 11 . . . . . . 7 (πœ‘ β†’ (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))):(((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)) Γ— (𝑋 Func π‘Œ))⟢((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
979, 33, 45, 96wunf 10725 . . . . . 6 (πœ‘ β†’ (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))) ∈ π‘ˆ)
989, 31, 97wunop 10720 . . . . 5 (πœ‘ β†’ ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩ ∈ π‘ˆ)
999, 25, 29, 98wuntp 10709 . . . 4 (πœ‘ β†’ {⟨(Baseβ€˜ndx), (𝑋 Func π‘Œ)⟩, ⟨(Hom β€˜ndx), (𝑋 Nat π‘Œ)⟩, ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩} ∈ π‘ˆ)
10017, 99eqeltrd 2832 . . 3 (πœ‘ β†’ 𝑄 ∈ π‘ˆ)
1011, 12, 15fuccat 17928 . . 3 (πœ‘ β†’ 𝑄 ∈ Cat)
102100, 101elind 4195 . 2 (πœ‘ β†’ 𝑄 ∈ (π‘ˆ ∩ Cat))
103102, 10eleqtrrd 2835 1 (πœ‘ β†’ 𝑄 ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   = wceq 1540   ∈ wcel 2105  βˆ€wral 3060  Vcvv 3473  [wsbc 3778  β¦‹csb 3894   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  {ctp 4633  βŸ¨cop 4635  βˆͺ cuni 4909   ↦ cmpt 5232   Γ— cxp 5675  ran crn 5678  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7412   ∈ cmpo 7414  Ο‰com 7858  1st c1st 7976  2nd c2nd 7977   ↑m cmap 8823   ↑pm cpm 8824  WUnicwun 10698  ndxcnx 17131  Basecbs 17149  Hom chom 17213  compcco 17214  Catccat 17613   Func cfunc 17809   Nat cnat 17897   FuncCat cfuc 17898  CatCatccatc 18053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-inf2 9639  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-oadd 8473  df-omul 8474  df-er 8706  df-ec 8708  df-qs 8712  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-wun 10700  df-ni 10870  df-pli 10871  df-mi 10872  df-lti 10873  df-plpq 10906  df-mpq 10907  df-ltpq 10908  df-enq 10909  df-nq 10910  df-erq 10911  df-plq 10912  df-mq 10913  df-1nq 10914  df-rq 10915  df-ltnq 10916  df-np 10979  df-plp 10981  df-ltp 10983  df-enr 11053  df-nr 11054  df-c 11119  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-nn 12218  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12478  df-z 12564  df-dec 12683  df-uz 12828  df-fz 13490  df-struct 17085  df-slot 17120  df-ndx 17132  df-base 17150  df-hom 17226  df-cco 17227  df-cat 17617  df-cid 17618  df-func 17813  df-nat 17899  df-fuc 17900  df-catc 18054
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator