Metamath Proof Explorer

Theorem wunfunc

Description: A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses wunfunc.1 ⊢ φ → U ∈ WUni
wunfunc.2 ⊢ φ → C ∈ U
wunfunc.3 ⊢ φ → D ∈ U
Assertion wunfunc ⊢ φ → C Func D ∈ U

Proof

Step Hyp Ref Expression
1 wunfunc.1 ⊢ φ → U ∈ WUni
2 wunfunc.2 ⊢ φ → C ∈ U
3 wunfunc.3 ⊢ φ → D ∈ U
4 df-base ⊢ Base = Slot 1
5 4 1 3 wunstr ⊢ φ → Base D ∈ U
6 4 1 2 wunstr ⊢ φ → Base C ∈ U
7 1 5 6 wunmap ⊢ φ → Base D Base C ∈ U
8 df-hom ⊢ Hom = Slot 14
9 8 1 2 wunstr ⊢ φ → Hom ⁡ C ∈ U
10 1 9 wunrn ⊢ φ → ran ⁡ Hom ⁡ C ∈ U
11 1 10 wununi ⊢ φ → ⋃ ran ⁡ Hom ⁡ C ∈ U
12 8 1 3 wunstr ⊢ φ → Hom ⁡ D ∈ U
13 1 12 wunrn ⊢ φ → ran ⁡ Hom ⁡ D ∈ U
14 1 13 wununi ⊢ φ → ⋃ ran ⁡ Hom ⁡ D ∈ U
15 1 11 14 wunxp ⊢ φ → ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D ∈ U
16 1 15 wunpw ⊢ φ → 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D ∈ U
17 1 6 6 wunxp ⊢ φ → Base C × Base C ∈ U
18 1 16 17 wunmap ⊢ φ → 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C ∈ U
19 1 7 18 wunxp ⊢ φ → Base D Base C × 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C ∈ U
20 relfunc ⊢ Rel ⁡ C Func D
21 20 a1i ⊢ φ → Rel ⁡ C Func D
22 df-br ⊢ f C Func D g ↔ f g ∈ C Func D
23 eqid ⊢ Base C = Base C
24 eqid ⊢ Base D = Base D
25 simpr ⊢ φ ∧ f C Func D g → f C Func D g
26 23 24 25 funcf1 ⊢ φ ∧ f C Func D g → f : Base C ⟶ Base D
27 fvex ⊢ Base D ∈ V
28 fvex ⊢ Base C ∈ V
29 27 28 elmap ⊢ f ∈ Base D Base C ↔ f : Base C ⟶ Base D
30 26 29 sylibr ⊢ φ ∧ f C Func D g → f ∈ Base D Base C
31 mapsspw ⊢ f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ⊆ 𝒫 Hom ⁡ C ⁡ z × f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z
32 fvssunirn ⊢ Hom ⁡ C ⁡ z ⊆ ⋃ ran ⁡ Hom ⁡ C
33 ovssunirn ⊢ f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z ⊆ ⋃ ran ⁡ Hom ⁡ D
34 xpss12 ⊢ Hom ⁡ C ⁡ z ⊆ ⋃ ran ⁡ Hom ⁡ C ∧ f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z ⊆ ⋃ ran ⁡ Hom ⁡ D → Hom ⁡ C ⁡ z × f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z ⊆ ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D
35 32 33 34 mp2an ⊢ Hom ⁡ C ⁡ z × f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z ⊆ ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D
36 35 sspwi ⊢ 𝒫 Hom ⁡ C ⁡ z × f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z ⊆ 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D
37 31 36 sstri ⊢ f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ⊆ 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D
38 37 rgenw ⊢ ∀ z ∈ Base C × Base C f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ⊆ 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D
39 ss2ixp ⊢ ∀ z ∈ Base C × Base C f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ⊆ 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D → ⨉ z ∈ Base C × Base C f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ⊆ ⨉ z ∈ Base C × Base C 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D
40 38 39 ax-mp ⊢ ⨉ z ∈ Base C × Base C f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ⊆ ⨉ z ∈ Base C × Base C 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D
41 28 28 xpex ⊢ Base C × Base C ∈ V
42 fvex ⊢ Hom ⁡ C ∈ V
43 42 rnex ⊢ ran ⁡ Hom ⁡ C ∈ V
44 43 uniex ⊢ ⋃ ran ⁡ Hom ⁡ C ∈ V
45 fvex ⊢ Hom ⁡ D ∈ V
46 45 rnex ⊢ ran ⁡ Hom ⁡ D ∈ V
47 46 uniex ⊢ ⋃ ran ⁡ Hom ⁡ D ∈ V
48 44 47 xpex ⊢ ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D ∈ V
49 48 pwex ⊢ 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D ∈ V
50 41 49 ixpconst ⊢ ⨉ z ∈ Base C × Base C 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D = 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C
51 40 50 sseqtri ⊢ ⨉ z ∈ Base C × Base C f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ⊆ 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C
52 eqid ⊢ Hom ⁡ C = Hom ⁡ C
53 eqid ⊢ Hom ⁡ D = Hom ⁡ D
54 23 52 53 25 funcixp ⊢ φ ∧ f C Func D g → g ∈ ⨉ z ∈ Base C × Base C f ⁡ 1 st ⁡ z Hom ⁡ D f ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z
55 51 54 sseldi ⊢ φ ∧ f C Func D g → g ∈ 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C
56 30 55 opelxpd ⊢ φ ∧ f C Func D g → f g ∈ Base D Base C × 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C
57 56 ex ⊢ φ → f C Func D g → f g ∈ Base D Base C × 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C
58 22 57 syl5bir ⊢ φ → f g ∈ C Func D → f g ∈ Base D Base C × 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C
59 21 58 relssdv ⊢ φ → C Func D ⊆ Base D Base C × 𝒫 ⋃ ran ⁡ Hom ⁡ C × ⋃ ran ⁡ Hom ⁡ D Base C × Base C
60 1 19 59 wunss ⊢ φ → C Func D ∈ U