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

Theorem catcfucclOLD 18103
Description: Obsolete proof of catcfuccl 18102 as of 14-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
catcfuccl.c 𝐢 = (CatCatβ€˜π‘ˆ)
catcfuccl.b 𝐡 = (Baseβ€˜πΆ)
catcfuccl.o 𝑄 = (𝑋 FuncCat π‘Œ)
catcfuccl.u (πœ‘ β†’ π‘ˆ ∈ WUni)
catcfuccl.1 (πœ‘ β†’ Ο‰ ∈ π‘ˆ)
catcfuccl.x (πœ‘ β†’ 𝑋 ∈ 𝐡)
catcfuccl.y (πœ‘ β†’ π‘Œ ∈ 𝐡)
Assertion
Ref Expression
catcfucclOLD (πœ‘ β†’ 𝑄 ∈ 𝐡)

Proof of Theorem catcfucclOLD
Dummy variables π‘Ž 𝑏 𝑓 𝑔 β„Ž 𝑣 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcfuccl.o . . . . 5 𝑄 = (𝑋 FuncCat π‘Œ)
2 eqid 2725 . . . . 5 (𝑋 Func π‘Œ) = (𝑋 Func π‘Œ)
3 eqid 2725 . . . . 5 (𝑋 Nat π‘Œ) = (𝑋 Nat π‘Œ)
4 eqid 2725 . . . . 5 (Baseβ€˜π‘‹) = (Baseβ€˜π‘‹)
5 eqid 2725 . . . . 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 18084 . . . . . . 7 (πœ‘ β†’ 𝐡 = (π‘ˆ ∩ Cat))
116, 10eleqtrd 2827 . . . . . 6 (πœ‘ β†’ 𝑋 ∈ (π‘ˆ ∩ Cat))
1211elin2d 4194 . . . . 5 (πœ‘ β†’ 𝑋 ∈ Cat)
13 catcfuccl.y . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ 𝐡)
1413, 10eleqtrd 2827 . . . . . 6 (πœ‘ β†’ π‘Œ ∈ (π‘ˆ ∩ Cat))
1514elin2d 4194 . . . . 5 (πœ‘ β†’ π‘Œ ∈ Cat)
16 eqidd 2726 . . . . 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 17943 . . . 4 (πœ‘ β†’ 𝑄 = {⟨(Baseβ€˜ndx), (𝑋 Func π‘Œ)⟩, ⟨(Hom β€˜ndx), (𝑋 Nat π‘Œ)⟩, ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩})
18 df-base 17175 . . . . . . 7 Base = Slot 1
19 catcfuccl.1 . . . . . . . 8 (πœ‘ β†’ Ο‰ ∈ π‘ˆ)
209, 19wunndx 17158 . . . . . . 7 (πœ‘ β†’ ndx ∈ π‘ˆ)
2118, 9, 20wunstr 17151 . . . . . 6 (πœ‘ β†’ (Baseβ€˜ndx) ∈ π‘ˆ)
2211elin1d 4193 . . . . . . 7 (πœ‘ β†’ 𝑋 ∈ π‘ˆ)
2314elin1d 4193 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ π‘ˆ)
249, 22, 23wunfunc 17881 . . . . . 6 (πœ‘ β†’ (𝑋 Func π‘Œ) ∈ π‘ˆ)
259, 21, 24wunop 10740 . . . . 5 (πœ‘ β†’ ⟨(Baseβ€˜ndx), (𝑋 Func π‘Œ)⟩ ∈ π‘ˆ)
26 df-hom 17251 . . . . . . 7 Hom = Slot 14
2726, 9, 20wunstr 17151 . . . . . 6 (πœ‘ β†’ (Hom β€˜ndx) ∈ π‘ˆ)
289, 22, 23wunnat 17940 . . . . . 6 (πœ‘ β†’ (𝑋 Nat π‘Œ) ∈ π‘ˆ)
299, 27, 28wunop 10740 . . . . 5 (πœ‘ β†’ ⟨(Hom β€˜ndx), (𝑋 Nat π‘Œ)⟩ ∈ π‘ˆ)
30 df-cco 17252 . . . . . . 7 comp = Slot 15
3130, 9, 20wunstr 17151 . . . . . 6 (πœ‘ β†’ (compβ€˜ndx) ∈ π‘ˆ)
329, 24, 24wunxp 10742 . . . . . . . 8 (πœ‘ β†’ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)) ∈ π‘ˆ)
339, 32, 24wunxp 10742 . . . . . . 7 (πœ‘ β†’ (((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)) Γ— (𝑋 Func π‘Œ)) ∈ π‘ˆ)
3430, 9, 23wunstr 17151 . . . . . . . . . . . . . 14 (πœ‘ β†’ (compβ€˜π‘Œ) ∈ π‘ˆ)
359, 34wunrn 10747 . . . . . . . . . . . . 13 (πœ‘ β†’ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
369, 35wununi 10724 . . . . . . . . . . . 12 (πœ‘ β†’ βˆͺ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
379, 36wunrn 10747 . . . . . . . . . . 11 (πœ‘ β†’ ran βˆͺ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
389, 37wununi 10724 . . . . . . . . . 10 (πœ‘ β†’ βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
399, 38wunpw 10725 . . . . . . . . 9 (πœ‘ β†’ 𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ∈ π‘ˆ)
4018, 9, 22wunstr 17151 . . . . . . . . 9 (πœ‘ β†’ (Baseβ€˜π‘‹) ∈ π‘ˆ)
419, 39, 40wunmap 10744 . . . . . . . 8 (πœ‘ β†’ (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ∈ π‘ˆ)
429, 28wunrn 10747 . . . . . . . . . 10 (πœ‘ β†’ ran (𝑋 Nat π‘Œ) ∈ π‘ˆ)
439, 42wununi 10724 . . . . . . . . 9 (πœ‘ β†’ βˆͺ ran (𝑋 Nat π‘Œ) ∈ π‘ˆ)
449, 43, 43wunxp 10742 . . . . . . . 8 (πœ‘ β†’ (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)) ∈ π‘ˆ)
459, 41, 44wunpm 10743 . . . . . . 7 (πœ‘ β†’ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))) ∈ π‘ˆ)
46 fvex 6903 . . . . . . . . . . 11 (1st β€˜π‘£) ∈ V
47 fvex 6903 . . . . . . . . . . . . . 14 (2nd β€˜π‘£) ∈ V
48 ovex 7446 . . . . . . . . . . . . . . . . 17 (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ∈ V
49 ovex 7446 . . . . . . . . . . . . . . . . . . . 20 (𝑋 Nat π‘Œ) ∈ V
5049rnex 7912 . . . . . . . . . . . . . . . . . . 19 ran (𝑋 Nat π‘Œ) ∈ V
5150uniex 7741 . . . . . . . . . . . . . . . . . 18 βˆͺ ran (𝑋 Nat π‘Œ) ∈ V
5251, 51xpex 7750 . . . . . . . . . . . . . . . . 17 (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)) ∈ V
53 eqid 2725 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))) = (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))
54 ovssunirn 7449 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) βŠ† βˆͺ ran (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))
55 ovssunirn 7449 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† βˆͺ ran (compβ€˜π‘Œ)
56 rnss 5936 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† βˆͺ ran (compβ€˜π‘Œ) β†’ ran (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯)) βŠ† ran βˆͺ ran (compβ€˜π‘Œ))
57 uniss 4912 . . . . . . . . . . . . . . . . . . . . . . . . 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 3983 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) βŠ† βˆͺ ran βˆͺ ran (compβ€˜π‘Œ)
60 ovex 7446 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) ∈ V
6160elpw 4603 . . . . . . . . . . . . . . . . . . . . . . 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 7115 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))):(Baseβ€˜π‘‹)βŸΆπ’« βˆͺ ran βˆͺ ran (compβ€˜π‘Œ)
65 fvex 6903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (compβ€˜π‘Œ) ∈ V
6665rnex 7912 . . . . . . . . . . . . . . . . . . . . . . . . 25 ran (compβ€˜π‘Œ) ∈ V
6766uniex 7741 . . . . . . . . . . . . . . . . . . . . . . . 24 βˆͺ ran (compβ€˜π‘Œ) ∈ V
6867rnex 7912 . . . . . . . . . . . . . . . . . . . . . . 23 ran βˆͺ ran (compβ€˜π‘Œ) ∈ V
6968uniex 7741 . . . . . . . . . . . . . . . . . . . . . 22 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ∈ V
7069pwex 5375 . . . . . . . . . . . . . . . . . . . . 21 𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ∈ V
71 fvex 6903 . . . . . . . . . . . . . . . . . . . . 21 (Baseβ€˜π‘‹) ∈ V
7270, 71elmap 8883 . . . . . . . . . . . . . . . . . . . 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 3056 . . . . . . . . . . . . . . . . . 18 βˆ€π‘ ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž)βˆ€π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔)(π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))) ∈ (𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹))
75 eqid 2725 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) = (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))
7675fmpo 8066 . . . . . . . . . . . . . . . . . 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 7449 . . . . . . . . . . . . . . . . . 18 (𝑔(𝑋 Nat π‘Œ)β„Ž) βŠ† βˆͺ ran (𝑋 Nat π‘Œ)
79 ovssunirn 7449 . . . . . . . . . . . . . . . . . 18 (𝑓(𝑋 Nat π‘Œ)𝑔) βŠ† βˆͺ ran (𝑋 Nat π‘Œ)
80 xpss12 5688 . . . . . . . . . . . . . . . . . 18 (((𝑔(𝑋 Nat π‘Œ)β„Ž) βŠ† βˆͺ ran (𝑋 Nat π‘Œ) ∧ (𝑓(𝑋 Nat π‘Œ)𝑔) βŠ† βˆͺ ran (𝑋 Nat π‘Œ)) β†’ ((𝑔(𝑋 Nat π‘Œ)β„Ž) Γ— (𝑓(𝑋 Nat π‘Œ)𝑔)) βŠ† (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))
8178, 79, 80mp2an 690 . . . . . . . . . . . . . . . . 17 ((𝑔(𝑋 Nat π‘Œ)β„Ž) Γ— (𝑓(𝑋 Nat π‘Œ)𝑔)) βŠ† (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))
82 elpm2r 8857 . . . . . . . . . . . . . . . . 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 691 . . . . . . . . . . . . . . . 16 (𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ)))
8483sbcth 3785 . . . . . . . . . . . . . . 15 ((2nd β€˜π‘£) ∈ V β†’ [(2nd β€˜π‘£) / 𝑔](𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
85 sbcel1g 4410 . . . . . . . . . . . . . . 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 3785 . . . . . . . . . . . 12 ((1st β€˜π‘£) ∈ V β†’ [(1st β€˜π‘£) / 𝑓]⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) ∈ ((𝒫 βˆͺ ran βˆͺ ran (compβ€˜π‘Œ) ↑m (Baseβ€˜π‘‹)) ↑pm (βˆͺ ran (𝑋 Nat π‘Œ) Γ— βˆͺ ran (𝑋 Nat π‘Œ))))
89 sbcel1g 4410 . . . . . . . . . . . 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 3056 . . . . . . . . 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 2725 . . . . . . . . . 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 8066 . . . . . . . . 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 10745 . . . . . 6 (πœ‘ β†’ (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))) ∈ π‘ˆ)
989, 31, 97wunop 10740 . . . . 5 (πœ‘ β†’ ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩ ∈ π‘ˆ)
999, 25, 29, 98wuntp 10729 . . . 4 (πœ‘ β†’ {⟨(Baseβ€˜ndx), (𝑋 Func π‘Œ)⟩, ⟨(Hom β€˜ndx), (𝑋 Nat π‘Œ)⟩, ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑋 Func π‘Œ) Γ— (𝑋 Func π‘Œ)), β„Ž ∈ (𝑋 Func π‘Œ) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑋 Nat π‘Œ)β„Ž), π‘Ž ∈ (𝑓(𝑋 Nat π‘Œ)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‹) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘Œ)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩} ∈ π‘ˆ)
10017, 99eqeltrd 2825 . . 3 (πœ‘ β†’ 𝑄 ∈ π‘ˆ)
1011, 12, 15fuccat 17956 . . 3 (πœ‘ β†’ 𝑄 ∈ Cat)
102100, 101elind 4189 . 2 (πœ‘ β†’ 𝑄 ∈ (π‘ˆ ∩ Cat))
103102, 10eleqtrrd 2828 1 (πœ‘ β†’ 𝑄 ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   = wceq 1533   ∈ wcel 2098  βˆ€wral 3051  Vcvv 3463  [wsbc 3770  β¦‹csb 3886   ∩ cin 3940   βŠ† wss 3941  π’« cpw 4599  {ctp 4629  βŸ¨cop 4631  βˆͺ cuni 4904   ↦ cmpt 5227   Γ— cxp 5671  ran crn 5674  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7413   ∈ cmpo 7415  Ο‰com 7865  1st c1st 7985  2nd c2nd 7986   ↑m cmap 8838   ↑pm cpm 8839  WUnicwun 10718  1c1 11134  4c4 12294  5c5 12295  cdc 12702  ndxcnx 17156  Basecbs 17174  Hom chom 17238  compcco 17239  Catccat 17638   Func cfunc 17834   Nat cnat 17925   FuncCat cfuc 17926  CatCatccatc 18081
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 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  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 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-omul 8485  df-er 8718  df-ec 8720  df-qs 8724  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-wun 10720  df-ni 10890  df-pli 10891  df-mi 10892  df-lti 10893  df-plpq 10926  df-mpq 10927  df-ltpq 10928  df-enq 10929  df-nq 10930  df-erq 10931  df-plq 10932  df-mq 10933  df-1nq 10934  df-rq 10935  df-ltnq 10936  df-np 10999  df-plp 11001  df-ltp 11003  df-enr 11073  df-nr 11074  df-c 11139  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-nn 12238  df-2 12300  df-3 12301  df-4 12302  df-5 12303  df-6 12304  df-7 12305  df-8 12306  df-9 12307  df-n0 12498  df-z 12584  df-dec 12703  df-uz 12848  df-fz 13512  df-struct 17110  df-slot 17145  df-ndx 17157  df-base 17175  df-hom 17251  df-cco 17252  df-cat 17642  df-cid 17643  df-func 17838  df-nat 17927  df-fuc 17928  df-catc 18082
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator