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 φ C Nat D 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 φ C Func D U
5 1 4 4 wunxp φ C Func D × C Func D U
6 df-hom Hom = Slot 14
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 = Slot 1
11 10 1 2 wunstr φ Base C U
12 1 9 11 wunmap φ ran Hom D Base C U
13 1 12 wunpw φ 𝒫 ran Hom D Base C U
14 fvex 1 st f V
15 fvex 1 st g V
16 ovex ran Hom D Base C V
17 ssrab2 a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x x Base C r x Hom D s x
18 ovssunirn r x Hom D s x ran Hom D
19 18 rgenw x Base C r x Hom D s x ran Hom D
20 ss2ixp x Base C r x Hom D s x ran Hom D x Base C r x Hom D s x x Base C ran Hom D
21 19 20 ax-mp x Base C r x Hom D s x x Base C ran Hom D
22 fvex Base C 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 Base C ran Hom D = ran Hom D Base C
27 21 26 sseqtri x Base C r x Hom D s x ran Hom D Base C
28 17 27 sstri a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x ran Hom D Base C
29 16 28 elpwi2 a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
30 29 sbcth 1 st g V [˙ 1 st g / s]˙ a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
31 sbcel1g 1 st g V [˙ 1 st g / s]˙ a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
32 30 31 mpbid 1 st g V 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
33 15 32 ax-mp 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
34 33 sbcth 1 st f V [˙ 1 st f / r]˙ 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
35 sbcel1g 1 st f V [˙ 1 st f / r]˙ 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C 1 st f / r 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
36 34 35 mpbid 1 st f V 1 st f / r 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
37 14 36 ax-mp 1 st f / r 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
38 37 rgen2w f C Func D g C Func D 1 st f / r 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C
39 eqid C Nat D = C Nat D
40 eqid Base C = Base C
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 C Nat D = f C Func D , g C Func D 1 st f / r 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x
45 44 fmpo f C Func D g C Func D 1 st f / r 1 st g / s a x Base C r x Hom D s x | x Base C y Base C z x Hom C y a y r x r y comp D s y x 2 nd f y z = x 2 nd g y z r x s x comp D s y a x 𝒫 ran Hom D Base C C Nat D : C Func D × C Func D 𝒫 ran Hom D Base C
46 38 45 mpbi C Nat D : C Func D × C Func D 𝒫 ran Hom D Base C
47 46 a1i φ C Nat D : C Func D × C Func D 𝒫 ran Hom D Base C
48 1 5 13 47 wunf φ C Nat D U