Metamath Proof Explorer

Theorem wunnatOLD

Description: Obsolete proof of wunnat as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses wunnat.1 ⊢φ→U∈WUni
wunnat.2 ⊢φ→C∈U
wunnat.3 ⊢φ→D∈U
Assertion wunnatOLD ⊢φ→CNatD∈U

Proof

Step Hyp Ref Expression
1 wunnat.1 ⊢φ→U∈WUni
2 wunnat.2 ⊢φ→C∈U
3 wunnat.3 ⊢φ→D∈U
4 1 2 3 wunfunc ⊢φ→CFuncD∈U
5 1 4 4 wunxp ⊢φ→CFuncD×CFuncD∈U
6 df-hom ⊢Hom=Slot14
7 6 1 3 wunstr ⊢φ→Hom⁡D∈U
8 1 7 wunrn ⊢φ→ran⁡Hom⁡D∈U
9 1 8 wununi ⊢φ→⋃ran⁡Hom⁡D∈U
10 df-base ⊢Base=Slot1
11 10 1 2 wunstr ⊢φ→BaseC∈U
12 1 9 11 wunmap ⊢φ→⋃ran⁡Hom⁡DBaseC∈U
13 1 12 wunpw ⊢φ→𝒫⋃ran⁡Hom⁡DBaseC∈U
14 fvex ⊢1st⁡f∈V
15 fvex ⊢1st⁡g∈V
16 ovex ⊢⋃ran⁡Hom⁡DBaseC∈V
17 ssrab2 ⊢a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x⊆⨉x∈BaseCr⁡xHom⁡Ds⁡x
18 ovssunirn ⊢r⁡xHom⁡Ds⁡x⊆⋃ran⁡Hom⁡D
19 18 rgenw ⊢∀x∈BaseCr⁡xHom⁡Ds⁡x⊆⋃ran⁡Hom⁡D
20 ss2ixp ⊢∀x∈BaseCr⁡xHom⁡Ds⁡x⊆⋃ran⁡Hom⁡D→⨉x∈BaseCr⁡xHom⁡Ds⁡x⊆⨉x∈BaseC⋃ran⁡Hom⁡D
21 19 20 ax-mp ⊢⨉x∈BaseCr⁡xHom⁡Ds⁡x⊆⨉x∈BaseC⋃ran⁡Hom⁡D
22 fvex ⊢BaseC∈V
23 fvex ⊢Hom⁡D∈V
24 23 rnex ⊢ran⁡Hom⁡D∈V
25 24 uniex ⊢⋃ran⁡Hom⁡D∈V
26 22 25 ixpconst ⊢⨉x∈BaseC⋃ran⁡Hom⁡D=⋃ran⁡Hom⁡DBaseC
27 21 26 sseqtri ⊢⨉x∈BaseCr⁡xHom⁡Ds⁡x⊆⋃ran⁡Hom⁡DBaseC
28 17 27 sstri ⊢a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x⊆⋃ran⁡Hom⁡DBaseC
29 16 28 elpwi2 ⊢a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
30 29 sbcth ⊢1st⁡g∈V→[˙1st⁡g/s]˙a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
31 sbcel1g ⊢1st⁡g∈V→[˙1st⁡g/s]˙a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC↔⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
32 30 31 mpbid ⊢1st⁡g∈V→⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
33 15 32 ax-mp ⊢⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
34 33 sbcth ⊢1st⁡f∈V→[˙1st⁡f/r]˙⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
35 sbcel1g ⊢1st⁡f∈V→[˙1st⁡f/r]˙⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC↔⦋1st⁡f/r⦌⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
36 34 35 mpbid ⊢1st⁡f∈V→⦋1st⁡f/r⦌⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
37 14 36 ax-mp ⊢⦋1st⁡f/r⦌⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
38 37 rgen2w ⊢∀f∈CFuncD∀g∈CFuncD⦋1st⁡f/r⦌⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC
39 eqid ⊢CNatD=CNatD
40 eqid ⊢BaseC=BaseC
41 eqid ⊢Hom⁡C=Hom⁡C
42 eqid ⊢Hom⁡D=Hom⁡D
43 eqid ⊢comp⁡D=comp⁡D
44 39 40 41 42 43 natfval ⊢CNatD=f∈CFuncD,g∈CFuncD⟼⦋1st⁡f/r⦌⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x
45 44 fmpo ⊢∀f∈CFuncD∀g∈CFuncD⦋1st⁡f/r⦌⦋1st⁡g/s⦌a∈⨉x∈BaseCr⁡xHom⁡Ds⁡x|∀x∈BaseC∀y∈BaseC∀z∈xHom⁡Cya⁡yr⁡xr⁡ycomp⁡Ds⁡yx2nd⁡fy⁡z=x2nd⁡gy⁡zr⁡xs⁡xcomp⁡Ds⁡ya⁡x∈𝒫⋃ran⁡Hom⁡DBaseC↔CNatD:CFuncD×CFuncD⟶𝒫⋃ran⁡Hom⁡DBaseC
46 38 45 mpbi ⊢CNatD:CFuncD×CFuncD⟶𝒫⋃ran⁡Hom⁡DBaseC
47 46 a1i ⊢φ→CNatD:CFuncD×CFuncD⟶𝒫⋃ran⁡Hom⁡DBaseC
48 1 5 13 47 wunf ⊢φ→CNatD∈U