wunfunc

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

	Ref	Expression
Hypotheses	wunfunc.1	$⊢ φ \to U \in WUni$
	wunfunc.2	$⊢ φ \to C \in U$
	wunfunc.3	$⊢ φ \to D \in U$
Assertion	wunfunc	$⊢ φ \to C Func D \in U$

Proof

Step	Hyp	Ref	Expression
1		wunfunc.1	$⊢ φ \to U \in WUni$
2		wunfunc.2	$⊢ φ \to C \in U$
3		wunfunc.3	$⊢ φ \to D \in U$
4		baseid	$⊢ Base = Slot {Base}_{ndx}$
5	4 1 3	wunstr	$⊢ φ \to {Base}_{D} \in U$
6	4 1 2	wunstr	$⊢ φ \to {Base}_{C} \in U$
7	1 5 6	wunmap	$⊢ φ \to {Base}_{D}^{{Base}_{C}} \in U$
8		homid	$⊢ Hom = Slot Hom (ndx)$
9	8 1 2	wunstr	$⊢ φ \to Hom (C) \in U$
10	1 9	wunrn	$⊢ φ \to ran Hom (C) \in U$
11	1 10	wununi	$⊢ φ \to ⋃ ran Hom (C) \in U$
12	8 1 3	wunstr	$⊢ φ \to Hom (D) \in U$
13	1 12	wunrn	$⊢ φ \to ran Hom (D) \in U$
14	1 13	wununi	$⊢ φ \to ⋃ ran Hom (D) \in U$
15	1 11 14	wunxp	$⊢ φ \to ⋃ ran Hom (C) \times ⋃ ran Hom (D) \in U$
16	1 15	wunpw	$⊢ φ \to 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D)) \in U$
17	1 6 6	wunxp	$⊢ φ \to {Base}_{C} \times {Base}_{C} \in U$
18	1 16 17	wunmap	$⊢ φ \to {𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})} \in U$
19	1 7 18	wunxp	$⊢ φ \to ({Base}_{D}^{{Base}_{C}}) \times ({𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})}) \in U$
20		relfunc	$⊢ Rel (C Func D)$
21	20	a1i	$⊢ φ \to Rel (C Func D)$
22		df-br	$⊢ f (C Func D) g \leftrightarrow ⟨f, g⟩ \in (C Func D)$
23		eqid	$⊢ {Base}_{C} = {Base}_{C}$
24		eqid	$⊢ {Base}_{D} = {Base}_{D}$
25		simpr	$⊢ (φ \land f (C Func D) g) \to f (C Func D) g$
26	23 24 25	funcf1	$⊢ (φ \land f (C Func D) g) \to f : {Base}_{C} ⟶ {Base}_{D}$
27		fvex	$⊢ {Base}_{D} \in V$
28		fvex	$⊢ {Base}_{C} \in V$
29	27 28	elmap	$⊢ f \in ({Base}_{D}^{{Base}_{C}}) \leftrightarrow f : {Base}_{C} ⟶ {Base}_{D}$
30	26 29	sylibr	$⊢ (φ \land f (C Func D) g) \to f \in ({Base}_{D}^{{Base}_{C}})$
31		mapsspw	$⊢ {(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (C) (z)} \subseteq 𝒫 (Hom (C) (z) \times (f (1^{st} (z)) Hom (D) f (2^{nd} (z))))$
32		fvssunirn	$⊢ Hom (C) (z) \subseteq ⋃ ran Hom (C)$
33		ovssunirn	$⊢ f (1^{st} (z)) Hom (D) f (2^{nd} (z)) \subseteq ⋃ ran Hom (D)$
34		xpss12	$⊢ (Hom (C) (z) \subseteq ⋃ ran Hom (C) \land f (1^{st} (z)) Hom (D) f (2^{nd} (z)) \subseteq ⋃ ran Hom (D)) \to Hom (C) (z) \times (f (1^{st} (z)) Hom (D) f (2^{nd} (z))) \subseteq ⋃ ran Hom (C) \times ⋃ ran Hom (D)$
35	32 33 34	mp2an	$⊢ Hom (C) (z) \times (f (1^{st} (z)) Hom (D) f (2^{nd} (z))) \subseteq ⋃ ran Hom (C) \times ⋃ ran Hom (D)$
36	35	sspwi	$⊢ 𝒫 (Hom (C) (z) \times (f (1^{st} (z)) Hom (D) f (2^{nd} (z)))) \subseteq 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))$
37	31 36	sstri	$⊢ {(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (C) (z)} \subseteq 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))$
38	37	rgenw	$⊢ \forall z \in ({Base}_{C} \times {Base}_{C}) {(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (C) (z)} \subseteq 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))$
39		ss2ixp	$⊢ \forall z \in ({Base}_{C} \times {Base}_{C}) {(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (C) (z)} \subseteq 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D)) \to \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (C) (z)}) \subseteq \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))$
40	38 39	ax-mp	$⊢ \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (C) (z)}) \subseteq \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))$
41	28 28	xpex	$⊢ {Base}_{C} \times {Base}_{C} \in V$
42		fvex	$⊢ Hom (C) \in V$
43	42	rnex	$⊢ ran Hom (C) \in V$
44	43	uniex	$⊢ ⋃ ran Hom (C) \in V$
45		fvex	$⊢ Hom (D) \in V$
46	45	rnex	$⊢ ran Hom (D) \in V$
47	46	uniex	$⊢ ⋃ ran Hom (D) \in V$
48	44 47	xpex	$⊢ ⋃ ran Hom (C) \times ⋃ ran Hom (D) \in V$
49	48	pwex	$⊢ 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D)) \in V$
50	41 49	ixpconst	$⊢ \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} 𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D)) = {𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})}$
51	40 50	sseqtri	$⊢ \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (C) (z)}) \subseteq {𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})}$
52		eqid	$⊢ Hom (C) = Hom (C)$
53		eqid	$⊢ Hom (D) = Hom (D)$
54	23 52 53 25	funcixp	$⊢ (φ \land f (C Func D) g) \to g \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (C) (z)})$
55	51 54	sselid	$⊢ (φ \land f (C Func D) g) \to g \in ({𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})})$
56	30 55	opelxpd	$⊢ (φ \land f (C Func D) g) \to ⟨f, g⟩ \in (({Base}_{D}^{{Base}_{C}}) \times ({𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})}))$
57	56	ex	$⊢ φ \to (f (C Func D) g \to ⟨f, g⟩ \in (({Base}_{D}^{{Base}_{C}}) \times ({𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})})))$
58	22 57	biimtrrid	$⊢ φ \to (⟨f, g⟩ \in (C Func D) \to ⟨f, g⟩ \in (({Base}_{D}^{{Base}_{C}}) \times ({𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})})))$
59	21 58	relssdv	$⊢ φ \to C Func D \subseteq ({Base}_{D}^{{Base}_{C}}) \times ({𝒫 (⋃ ran Hom (C) \times ⋃ ran Hom (D))}^{({Base}_{C} \times {Base}_{C})})$
60	1 19 59	wunss	$⊢ φ \to C Func D \in U$

Metamath Proof Explorer

Theorem wunfunc

Proof