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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcfuccl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catcfuccl.o	⊢ 𝑄 = ( 𝑋 FuncCat 𝑌 )
	catcfuccl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	catcfuccl.1	⊢ ( 𝜑 → ω ∈ 𝑈 )
	catcfuccl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	catcfuccl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	catcfuccl	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		catcfuccl.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcfuccl.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		catcfuccl.o	⊢ 𝑄 = ( 𝑋 FuncCat 𝑌 )
4		catcfuccl.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
5		catcfuccl.1	⊢ ( 𝜑 → ω ∈ 𝑈 )
6		catcfuccl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		catcfuccl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		eqid	⊢ ( 𝑋 Func 𝑌 ) = ( 𝑋 Func 𝑌 )
9		eqid	⊢ ( 𝑋 Nat 𝑌 ) = ( 𝑋 Nat 𝑌 )
10		eqid	⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
11		eqid	⊢ ( comp ‘ 𝑌 ) = ( comp ‘ 𝑌 )
12	1 2 4	catcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
13	6 12	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
14	13	elin2d	⊢ ( 𝜑 → 𝑋 ∈ Cat )
15	7 12	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑈 ∩ Cat ) )
16	15	elin2d	⊢ ( 𝜑 → 𝑌 ∈ Cat )
17		eqidd	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
18	3 8 9 10 11 14 16 17	fucval	⊢ ( 𝜑 → 𝑄 = { ⟨ ( Base ‘ ndx ) , ( 𝑋 Func 𝑌 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑋 Nat 𝑌 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
19		baseid	⊢ Base = Slot ( Base ‘ ndx )
20	4 5	wunndx	⊢ ( 𝜑 → ndx ∈ 𝑈 )
21	19 4 20	wunstr	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
22	1 2 4 6	catcbascl	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
23	1 2 4 7	catcbascl	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
24	4 22 23	wunfunc	⊢ ( 𝜑 → ( 𝑋 Func 𝑌 ) ∈ 𝑈 )
25	4 21 24	wunop	⊢ ( 𝜑 → ⟨ ( Base ‘ ndx ) , ( 𝑋 Func 𝑌 ) ⟩ ∈ 𝑈 )
26		homid	⊢ Hom = Slot ( Hom ‘ ndx )
27	26 4 20	wunstr	⊢ ( 𝜑 → ( Hom ‘ ndx ) ∈ 𝑈 )
28	4 22 23	wunnat	⊢ ( 𝜑 → ( 𝑋 Nat 𝑌 ) ∈ 𝑈 )
29	4 27 28	wunop	⊢ ( 𝜑 → ⟨ ( Hom ‘ ndx ) , ( 𝑋 Nat 𝑌 ) ⟩ ∈ 𝑈 )
30		ccoid	⊢ comp = Slot ( comp ‘ ndx )
31	30 4 20	wunstr	⊢ ( 𝜑 → ( comp ‘ ndx ) ∈ 𝑈 )
32	4 24 24	wunxp	⊢ ( 𝜑 → ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) ∈ 𝑈 )
33	4 32 24	wunxp	⊢ ( 𝜑 → ( ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) × ( 𝑋 Func 𝑌 ) ) ∈ 𝑈 )
34	1 2 4 7	catcccocl	⊢ ( 𝜑 → ( comp ‘ 𝑌 ) ∈ 𝑈 )
35	4 34	wunrn	⊢ ( 𝜑 → ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
36	4 35	wununi	⊢ ( 𝜑 → ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
37	4 36	wunrn	⊢ ( 𝜑 → ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
38	4 37	wununi	⊢ ( 𝜑 → ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
39	4 38	wunpw	⊢ ( 𝜑 → 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ 𝑈 )
40	1 2 4 6	catcbaselcl	⊢ ( 𝜑 → ( Base ‘ 𝑋 ) ∈ 𝑈 )
41	4 39 40	wunmap	⊢ ( 𝜑 → ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ∈ 𝑈 )
42	4 28	wunrn	⊢ ( 𝜑 → ran ( 𝑋 Nat 𝑌 ) ∈ 𝑈 )
43	4 42	wununi	⊢ ( 𝜑 → ∪ ran ( 𝑋 Nat 𝑌 ) ∈ 𝑈 )
44	4 43 43	wunxp	⊢ ( 𝜑 → ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ∈ 𝑈 )
45	4 41 44	wunpm	⊢ ( 𝜑 → ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) ∈ 𝑈 )
46		fvex	⊢ ( 1^st ‘ 𝑣 ) ∈ V
47		fvex	⊢ ( 2^nd ‘ 𝑣 ) ∈ V
48		ovex	⊢ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ∈ V
49		ovex	⊢ ( 𝑋 Nat 𝑌 ) ∈ V
50	49	rnex	⊢ ran ( 𝑋 Nat 𝑌 ) ∈ V
51	50	uniex	⊢ ∪ ran ( 𝑋 Nat 𝑌 ) ∈ V
52	51 51	xpex	⊢ ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ∈ V
53		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) )
54		ovssunirn	⊢ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ⊆ ∪ ran ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) )
55		ovssunirn	⊢ ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ⊆ ∪ ran ( comp ‘ 𝑌 )
56		rnss	⊢ ( ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ⊆ ∪ ran ( comp ‘ 𝑌 ) → ran ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑌 ) )
57		uniss	⊢ ( ran ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ⊆ ran ∪ ran ( comp ‘ 𝑌 ) → ∪ ran ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
58	55 56 57	mp2b	⊢ ∪ ran ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 )
59	54 58	sstri	⊢ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 )
60		ovex	⊢ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ∈ V
61	60	elpw	⊢ ( ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↔ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
62	59 61	mpbir	⊢ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 )
63	62	a1i	⊢ ( 𝑥 ∈ ( Base ‘ 𝑋 ) → ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ∈ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
64	53 63	fmpti	⊢ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) : ( Base ‘ 𝑋 ) ⟶ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 )
65		fvex	⊢ ( comp ‘ 𝑌 ) ∈ V
66	65	rnex	⊢ ran ( comp ‘ 𝑌 ) ∈ V
67	66	uniex	⊢ ∪ ran ( comp ‘ 𝑌 ) ∈ V
68	67	rnex	⊢ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
69	68	uniex	⊢ ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
70	69	pwex	⊢ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ∈ V
71		fvex	⊢ ( Base ‘ 𝑋 ) ∈ V
72	70 71	elmap	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) : ( Base ‘ 𝑋 ) ⟶ 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) )
73	64 72	mpbir	⊢ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) )
74	73	rgen2w	⊢ ∀ 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) ∀ 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) )
75		eqid	⊢ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
76	75	fmpo	⊢ ( ∀ 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) ∀ 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↔ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) : ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⟶ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) )
77	74 76	mpbi	⊢ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) : ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⟶ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) )
78		ovssunirn	⊢ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) ⊆ ∪ ran ( 𝑋 Nat 𝑌 )
79		ovssunirn	⊢ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ⊆ ∪ ran ( 𝑋 Nat 𝑌 )
80		xpss12	⊢ ( ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) ⊆ ∪ ran ( 𝑋 Nat 𝑌 ) ∧ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ⊆ ∪ ran ( 𝑋 Nat 𝑌 ) ) → ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⊆ ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) )
81	78 79 80	mp2an	⊢ ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⊆ ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) )
82		elpm2r	⊢ ( ( ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ∈ V ∧ ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ∈ V ) ∧ ( ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) : ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⟶ ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ∧ ( ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) × ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ) ⊆ ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) ) → ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) )
83	48 52 77 81 82	mp4an	⊢ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) )
84	83	sbcth	⊢ ( ( 2^nd ‘ 𝑣 ) ∈ V → [ ( 2^nd ‘ 𝑣 ) / 𝑔 ] ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) )
85		sbcel1g	⊢ ( ( 2^nd ‘ 𝑣 ) ∈ V → ( [ ( 2^nd ‘ 𝑣 ) / 𝑔 ] ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) ↔ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) ) )
86	84 85	mpbid	⊢ ( ( 2^nd ‘ 𝑣 ) ∈ V → ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) )
87	47 86	ax-mp	⊢ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) )
88	87	sbcth	⊢ ( ( 1^st ‘ 𝑣 ) ∈ V → [ ( 1^st ‘ 𝑣 ) / 𝑓 ] ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) )
89		sbcel1g	⊢ ( ( 1^st ‘ 𝑣 ) ∈ V → ( [ ( 1^st ‘ 𝑣 ) / 𝑓 ] ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) ↔ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) ) )
90	88 89	mpbid	⊢ ( ( 1^st ‘ 𝑣 ) ∈ V → ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) )
91	46 90	ax-mp	⊢ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) )
92	91	rgen2w	⊢ ∀ 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) ∀ ℎ ∈ ( 𝑋 Func 𝑌 ) ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) )
93		eqid	⊢ ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
94	93	fmpo	⊢ ( ∀ 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) ∀ ℎ ∈ ( 𝑋 Func 𝑌 ) ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) ↔ ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) : ( ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) × ( 𝑋 Func 𝑌 ) ) ⟶ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) )
95	92 94	mpbi	⊢ ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) : ( ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) × ( 𝑋 Func 𝑌 ) ) ⟶ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) )
96	95	a1i	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) : ( ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) × ( 𝑋 Func 𝑌 ) ) ⟶ ( ( 𝒫 ∪ ran ∪ ran ( comp ‘ 𝑌 ) ↑_m ( Base ‘ 𝑋 ) ) ↑_pm ( ∪ ran ( 𝑋 Nat 𝑌 ) × ∪ ran ( 𝑋 Nat 𝑌 ) ) ) )
97	4 33 45 96	wunf	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ 𝑈 )
98	4 31 97	wunop	⊢ ( 𝜑 → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ ∈ 𝑈 )
99	4 25 29 98	wuntp	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , ( 𝑋 Func 𝑌 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑋 Nat 𝑌 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑋 Func 𝑌 ) × ( 𝑋 Func 𝑌 ) ) , ℎ ∈ ( 𝑋 Func 𝑌 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑋 Nat 𝑌 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑋 Nat 𝑌 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑋 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑌 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } ∈ 𝑈 )
100	18 99	eqeltrd	⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
101	3 14 16	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
102	100 101	elind	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑈 ∩ Cat ) )
103	102 12	eleqtrrd	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )

Metamath Proof Explorer

Theorem catcfuccl

Proof