Metamath Proof Explorer

Theorem wunnat

Description: A weak universe is closed under the natural transformation operation. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof shortened by AV, 13-Oct-2024)

Ref Expression
Hypotheses wunnat.1 ⊢ φ → U ∈ WUni
wunnat.2 ⊢ φ → C ∈ U
wunnat.3 ⊢ φ → D ∈ U
Assertion wunnat ⊢ φ → 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 homid ⊢ Hom = Slot Hom ⁡ ndx
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 baseid ⊢ Base = Slot Base ndx
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