catcfuccl

Description: The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof shortened by AV, 14-Oct-2024)

	Ref	Expression
Hypotheses	catcfuccl.c	$⊢ C = CatCat (U)$
	catcfuccl.b	$⊢ B = {Base}_{C}$
	catcfuccl.o	$⊢ Q = X FuncCat Y$
	catcfuccl.u	$⊢ φ \to U \in WUni$
	catcfuccl.1	$⊢ φ \to ω \in U$
	catcfuccl.x	$⊢ φ \to X \in B$
	catcfuccl.y	$⊢ φ \to Y \in B$
Assertion	catcfuccl	$⊢ φ \to Q \in B$

Proof

Step	Hyp	Ref	Expression
1		catcfuccl.c	$⊢ C = CatCat (U)$
2		catcfuccl.b	$⊢ B = {Base}_{C}$
3		catcfuccl.o	$⊢ Q = X FuncCat Y$
4		catcfuccl.u	$⊢ φ \to U \in WUni$
5		catcfuccl.1	$⊢ φ \to ω \in U$
6		catcfuccl.x	$⊢ φ \to X \in B$
7		catcfuccl.y	$⊢ φ \to Y \in B$
8		eqid	$⊢ X Func Y = X Func Y$
9		eqid	$⊢ X Nat Y = X Nat Y$
10		eqid	$⊢ {Base}_{X} = {Base}_{X}$
11		eqid	$⊢ comp (Y) = comp (Y)$
12	1 2 4	catcbas	$⊢ φ \to B = U \cap Cat$
13	6 12	eleqtrd	$⊢ φ \to X \in (U \cap Cat)$
14	13	elin2d	$⊢ φ \to X \in Cat$
15	7 12	eleqtrd	$⊢ φ \to Y \in (U \cap Cat)$
16	15	elin2d	$⊢ φ \to Y \in Cat$
17		eqidd	$⊢ φ \to (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)))) = (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))))$
18	3 8 9 10 11 14 16 17	fucval	$⊢ φ \to Q = \{⟨{Base}_{ndx}, X Func Y⟩, ⟨Hom (ndx), X Nat Y⟩, ⟨comp (ndx), (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))))⟩\}$
19		baseid	$⊢ Base = Slot {Base}_{ndx}$
20	4 5	wunndx	$⊢ φ \to ndx \in U$
21	19 4 20	wunstr	$⊢ φ \to {Base}_{ndx} \in U$
22	1 2 4 6	catcbascl	$⊢ φ \to X \in U$
23	1 2 4 7	catcbascl	$⊢ φ \to Y \in U$
24	4 22 23	wunfunc	$⊢ φ \to X Func Y \in U$
25	4 21 24	wunop	$⊢ φ \to ⟨{Base}_{ndx}, X Func Y⟩ \in U$
26		homid	$⊢ Hom = Slot Hom (ndx)$
27	26 4 20	wunstr	$⊢ φ \to Hom (ndx) \in U$
28	4 22 23	wunnat	$⊢ φ \to X Nat Y \in U$
29	4 27 28	wunop	$⊢ φ \to ⟨Hom (ndx), X Nat Y⟩ \in U$
30		ccoid	$⊢ comp = Slot comp (ndx)$
31	30 4 20	wunstr	$⊢ φ \to comp (ndx) \in U$
32	4 24 24	wunxp	$⊢ φ \to (X Func Y) \times (X Func Y) \in U$
33	4 32 24	wunxp	$⊢ φ \to ((X Func Y) \times (X Func Y)) \times (X Func Y) \in U$
34	1 2 4 7	catcccocl	$⊢ φ \to comp (Y) \in U$
35	4 34	wunrn	$⊢ φ \to ran comp (Y) \in U$
36	4 35	wununi	$⊢ φ \to ⋃ ran comp (Y) \in U$
37	4 36	wunrn	$⊢ φ \to ran ⋃ ran comp (Y) \in U$
38	4 37	wununi	$⊢ φ \to ⋃ ran ⋃ ran comp (Y) \in U$
39	4 38	wunpw	$⊢ φ \to 𝒫 ⋃ ran ⋃ ran comp (Y) \in U$
40	1 2 4 6	catcbaselcl	$⊢ φ \to {Base}_{X} \in U$
41	4 39 40	wunmap	$⊢ φ \to {𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}} \in U$
42	4 28	wunrn	$⊢ φ \to ran (X Nat Y) \in U$
43	4 42	wununi	$⊢ φ \to ⋃ ran (X Nat Y) \in U$
44	4 43 43	wunxp	$⊢ φ \to ⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y) \in U$
45	4 41 44	wunpm	$⊢ φ \to ({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)) \in U$
46		fvex	$⊢ 1^{st} (v) \in V$
47		fvex	$⊢ 2^{nd} (v) \in V$
48		ovex	$⊢ {𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}} \in V$
49		ovex	$⊢ X Nat Y \in V$
50	49	rnex	$⊢ ran (X Nat Y) \in V$
51	50	uniex	$⊢ ⋃ ran (X Nat Y) \in V$
52	51 51	xpex	$⊢ ⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y) \in V$
53		eqid	$⊢ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)) = (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))$
54		ovssunirn	$⊢ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x) \subseteq ⋃ ran (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x))$
55		ovssunirn	$⊢ ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x) \subseteq ⋃ ran comp (Y)$
56		rnss	$⊢ ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x) \subseteq ⋃ ran comp (Y) \to ran (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) \subseteq ran ⋃ ran comp (Y)$
57		uniss	$⊢ ran (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) \subseteq ran ⋃ ran comp (Y) \to ⋃ ran (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) \subseteq ⋃ ran ⋃ ran comp (Y)$
58	55 56 57	mp2b	$⊢ ⋃ ran (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) \subseteq ⋃ ran ⋃ ran comp (Y)$
59	54 58	sstri	$⊢ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x) \subseteq ⋃ ran ⋃ ran comp (Y)$
60		ovex	$⊢ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x) \in V$
61	60	elpw	$⊢ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x) \in 𝒫 ⋃ ran ⋃ ran comp (Y) \leftrightarrow b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x) \subseteq ⋃ ran ⋃ ran comp (Y)$
62	59 61	mpbir	$⊢ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x) \in 𝒫 ⋃ ran ⋃ ran comp (Y)$
63	62	a1i	$⊢ x \in {Base}_{X} \to b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x) \in 𝒫 ⋃ ran ⋃ ran comp (Y)$
64	53 63	fmpti	$⊢ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)) : {Base}_{X} ⟶ 𝒫 ⋃ ran ⋃ ran comp (Y)$
65		fvex	$⊢ comp (Y) \in V$
66	65	rnex	$⊢ ran comp (Y) \in V$
67	66	uniex	$⊢ ⋃ ran comp (Y) \in V$
68	67	rnex	$⊢ ran ⋃ ran comp (Y) \in V$
69	68	uniex	$⊢ ⋃ ran ⋃ ran comp (Y) \in V$
70	69	pwex	$⊢ 𝒫 ⋃ ran ⋃ ran comp (Y) \in V$
71		fvex	$⊢ {Base}_{X} \in V$
72	70 71	elmap	$⊢ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)) \in ({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) \leftrightarrow (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)) : {Base}_{X} ⟶ 𝒫 ⋃ ran ⋃ ran comp (Y)$
73	64 72	mpbir	$⊢ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)) \in ({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}})$
74	73	rgen2w	$⊢ \forall b \in (g (X Nat Y) h) \forall a \in (f (X Nat Y) g) (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)) \in ({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}})$
75		eqid	$⊢ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) = (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)))$
76	75	fmpo	$⊢ \forall b \in (g (X Nat Y) h) \forall a \in (f (X Nat Y) g) (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)) \in ({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) \leftrightarrow (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) : (g (X Nat Y) h) \times (f (X Nat Y) g) ⟶ {𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}$
77	74 76	mpbi	$⊢ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) : (g (X Nat Y) h) \times (f (X Nat Y) g) ⟶ {𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}$
78		ovssunirn	$⊢ g (X Nat Y) h \subseteq ⋃ ran (X Nat Y)$
79		ovssunirn	$⊢ f (X Nat Y) g \subseteq ⋃ ran (X Nat Y)$
80		xpss12	$⊢ (g (X Nat Y) h \subseteq ⋃ ran (X Nat Y) \land f (X Nat Y) g \subseteq ⋃ ran (X Nat Y)) \to (g (X Nat Y) h) \times (f (X Nat Y) g) \subseteq ⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)$
81	78 79 80	mp2an	$⊢ (g (X Nat Y) h) \times (f (X Nat Y) g) \subseteq ⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)$
82		elpm2r	$⊢ (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}} \in V \land ⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y) \in V) \land ((b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) : (g (X Nat Y) h) \times (f (X Nat Y) g) ⟶ {𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}} \land (g (X Nat Y) h) \times (f (X Nat Y) g) \subseteq ⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))) \to (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
83	48 52 77 81 82	mp4an	$⊢ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
84	83	sbcth	$⊢ 2^{nd} (v) \in V \to \underset{˙}{[} 2^{nd} (v) / g \underset{˙}{]} (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
85		sbcel1g	$⊢ 2^{nd} (v) \in V \to (\underset{˙}{[} 2^{nd} (v) / g \underset{˙}{]} (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))) \leftrightarrow ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))))$
86	84 85	mpbid	$⊢ 2^{nd} (v) \in V \to ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
87	47 86	ax-mp	$⊢ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
88	87	sbcth	$⊢ 1^{st} (v) \in V \to \underset{˙}{[} 1^{st} (v) / f \underset{˙}{]} ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
89		sbcel1g	$⊢ 1^{st} (v) \in V \to (\underset{˙}{[} 1^{st} (v) / f \underset{˙}{]} ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))) \leftrightarrow ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))))$
90	88 89	mpbid	$⊢ 1^{st} (v) \in V \to ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
91	46 90	ax-mp	$⊢ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
92	91	rgen2w	$⊢ \forall v \in ((X Func Y) \times (X Func Y)) \forall h \in (X Func Y) ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y)))$
93		eqid	$⊢ (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)))) = (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))))$
94	93	fmpo	$⊢ \forall v \in ((X Func Y) \times (X Func Y)) \forall h \in (X Func Y) ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))) \in (({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))) \leftrightarrow (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)))) : ((X Func Y) \times (X Func Y)) \times (X Func Y) ⟶ ({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))$
95	92 94	mpbi	$⊢ (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)))) : ((X Func Y) \times (X Func Y)) \times (X Func Y) ⟶ ({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))$
96	95	a1i	$⊢ φ \to (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)))) : ((X Func Y) \times (X Func Y)) \times (X Func Y) ⟶ ({𝒫 ⋃ ran ⋃ ran comp (Y)}^{{Base}_{X}}) ↑_{𝑝𝑚} (⋃ ran (X Nat Y) \times ⋃ ran (X Nat Y))$
97	4 33 45 96	wunf	$⊢ φ \to (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x)))) \in U$
98	4 31 97	wunop	$⊢ φ \to ⟨comp (ndx), (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))))⟩ \in U$
99	4 25 29 98	wuntp	$⊢ φ \to \{⟨{Base}_{ndx}, X Func Y⟩, ⟨Hom (ndx), X Nat Y⟩, ⟨comp (ndx), (v \in ((X Func Y) \times (X Func Y)), h \in (X Func Y) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (X Nat Y) h), a \in (f (X Nat Y) g) ⟼ (x \in {Base}_{X} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (Y) 1^{st} (h) (x)) a (x))))⟩\} \in U$
100	18 99	eqeltrd	$⊢ φ \to Q \in U$
101	3 14 16	fuccat	$⊢ φ \to Q \in Cat$
102	100 101	elind	$⊢ φ \to Q \in (U \cap Cat)$
103	102 12	eleqtrrd	$⊢ φ \to Q \in B$

Metamath Proof Explorer

Theorem catcfuccl

Proof