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	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wunfunc.2	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	wunfunc.3	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
Assertion	wunfunc	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wunfunc.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wunfunc.2	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
3		wunfunc.3	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
4		baseid	⊢ Base = Slot ( Base ‘ ndx )
5	4 1 3	wunstr	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) ∈ 𝑈 )
6	4 1 2	wunstr	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) ∈ 𝑈 )
7	1 5 6	wunmap	⊢ ( 𝜑 → ( ( Base ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) ∈ 𝑈 )
8		homid	⊢ Hom = Slot ( Hom ‘ ndx )
9	8 1 2	wunstr	⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) ∈ 𝑈 )
10	1 9	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝐶 ) ∈ 𝑈 )
11	1 10	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝐶 ) ∈ 𝑈 )
12	8 1 3	wunstr	⊢ ( 𝜑 → ( Hom ‘ 𝐷 ) ∈ 𝑈 )
13	1 12	wunrn	⊢ ( 𝜑 → ran ( Hom ‘ 𝐷 ) ∈ 𝑈 )
14	1 13	wununi	⊢ ( 𝜑 → ∪ ran ( Hom ‘ 𝐷 ) ∈ 𝑈 )
15	1 11 14	wunxp	⊢ ( 𝜑 → ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ∈ 𝑈 )
16	1 15	wunpw	⊢ ( 𝜑 → 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ∈ 𝑈 )
17	1 6 6	wunxp	⊢ ( 𝜑 → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ 𝑈 )
18	1 16 17	wunmap	⊢ ( 𝜑 → ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ∈ 𝑈 )
19	1 7 18	wunxp	⊢ ( 𝜑 → ( ( ( Base ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) × ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ∈ 𝑈 )
20		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
21	20	a1i	⊢ ( 𝜑 → Rel ( 𝐶 Func 𝐷 ) )
22		df-br	⊢ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ↔ ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
23		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
24		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) → 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 )
26	23 24 25	funcf1	⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) → 𝑓 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
27		fvex	⊢ ( Base ‘ 𝐷 ) ∈ V
28		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
29	27 28	elmap	⊢ ( 𝑓 ∈ ( ( Base ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) ↔ 𝑓 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
30	26 29	sylibr	⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) → 𝑓 ∈ ( ( Base ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) )
31		mapsspw	⊢ ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ⊆ 𝒫 ( ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) × ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) )
32		fvssunirn	⊢ ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ⊆ ∪ ran ( Hom ‘ 𝐶 )
33		ovssunirn	⊢ ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ⊆ ∪ ran ( Hom ‘ 𝐷 )
34		xpss12	⊢ ( ( ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ⊆ ∪ ran ( Hom ‘ 𝐶 ) ∧ ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ⊆ ∪ ran ( Hom ‘ 𝐷 ) ) → ( ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) × ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ) ⊆ ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) )
35	32 33 34	mp2an	⊢ ( ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) × ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ) ⊆ ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) )
36	35	sspwi	⊢ 𝒫 ( ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) × ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ) ⊆ 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) )
37	31 36	sstri	⊢ ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ⊆ 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) )
38	37	rgenw	⊢ ∀ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ⊆ 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) )
39		ss2ixp	⊢ ( ∀ 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ⊆ 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) → X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ⊆ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) )
40	38 39	ax-mp	⊢ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ⊆ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) )
41	28 28	xpex	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∈ V
42		fvex	⊢ ( Hom ‘ 𝐶 ) ∈ V
43	42	rnex	⊢ ran ( Hom ‘ 𝐶 ) ∈ V
44	43	uniex	⊢ ∪ ran ( Hom ‘ 𝐶 ) ∈ V
45		fvex	⊢ ( Hom ‘ 𝐷 ) ∈ V
46	45	rnex	⊢ ran ( Hom ‘ 𝐷 ) ∈ V
47	46	uniex	⊢ ∪ ran ( Hom ‘ 𝐷 ) ∈ V
48	44 47	xpex	⊢ ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ∈ V
49	48	pwex	⊢ 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ∈ V
50	41 49	ixpconst	⊢ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) = ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
51	40 50	sseqtri	⊢ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ⊆ ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
52		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
53		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
54	23 52 53 25	funcixp	⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) → 𝑔 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝑓 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) )
55	51 54	sselid	⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) → 𝑔 ∈ ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
56	30 55	opelxpd	⊢ ( ( 𝜑 ∧ 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ) → ⟨ 𝑓 , 𝑔 ⟩ ∈ ( ( ( Base ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) × ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) )
57	56	ex	⊢ ( 𝜑 → ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 → ⟨ 𝑓 , 𝑔 ⟩ ∈ ( ( ( Base ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) × ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ) )
58	22 57	syl5bir	⊢ ( 𝜑 → ( ⟨ 𝑓 , 𝑔 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ⟨ 𝑓 , 𝑔 ⟩ ∈ ( ( ( Base ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) × ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) ) )
59	21 58	relssdv	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) ⊆ ( ( ( Base ‘ 𝐷 ) ↑_m ( Base ‘ 𝐶 ) ) × ( 𝒫 ( ∪ ran ( Hom ‘ 𝐶 ) × ∪ ran ( Hom ‘ 𝐷 ) ) ↑_m ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) ) )
60	1 19 59	wunss	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) ∈ 𝑈 )

Metamath Proof Explorer

Theorem wunfunc

Proof