Theorem wunfunc 16382

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

Hypotheses

Ref	Expression
wunfunc.1	⊢ (𝜑 → 𝑈 ∈ WUni)
wunfunc.2	⊢ (𝜑 → 𝐶 ∈ 𝑈)
wunfunc.3	⊢ (𝜑 → 𝐷 ∈ 𝑈)

Assertion

Ref	Expression
wunfunc	⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈)

Proof of Theorem wunfunc

Dummy variables 𝑓 𝑔 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wunfunc.1	. 2 ⊢ (𝜑 → 𝑈 ∈ WUni)
2		df-base 15700	. . . . 5 ⊢ Base = Slot 1
3		wunfunc.3	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ 𝑈)
4	2, 1, 3	wunstr 15714	. . . 4 ⊢ (𝜑 → (Base‘𝐷) ∈ 𝑈)
5		wunfunc.2	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑈)
6	2, 1, 5	wunstr 15714	. . . 4 ⊢ (𝜑 → (Base‘𝐶) ∈ 𝑈)
7	1, 4, 6	wunmap 9427	. . 3 ⊢ (𝜑 → ((Base‘𝐷) ↑𝑚 (Base‘𝐶)) ∈ 𝑈)
8		df-hom 15793	. . . . . . . . 9 ⊢ Hom = Slot ;14
9	8, 1, 5	wunstr 15714	. . . . . . . 8 ⊢ (𝜑 → (Hom ‘𝐶) ∈ 𝑈)
10	1, 9	wunrn 9430	. . . . . . 7 ⊢ (𝜑 → ran (Hom ‘𝐶) ∈ 𝑈)
11	1, 10	wununi 9407	. . . . . 6 ⊢ (𝜑 → ∪ ran (Hom ‘𝐶) ∈ 𝑈)
12	8, 1, 3	wunstr 15714	. . . . . . . 8 ⊢ (𝜑 → (Hom ‘𝐷) ∈ 𝑈)
13	1, 12	wunrn 9430	. . . . . . 7 ⊢ (𝜑 → ran (Hom ‘𝐷) ∈ 𝑈)
14	1, 13	wununi 9407	. . . . . 6 ⊢ (𝜑 → ∪ ran (Hom ‘𝐷) ∈ 𝑈)
15	1, 11, 14	wunxp 9425	. . . . 5 ⊢ (𝜑 → (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ∈ 𝑈)
16	1, 15	wunpw 9408	. . . 4 ⊢ (𝜑 → 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ∈ 𝑈)
17	1, 6, 6	wunxp 9425	. . . 4 ⊢ (𝜑 → ((Base‘𝐶) × (Base‘𝐶)) ∈ 𝑈)
18	1, 16, 17	wunmap 9427	. . 3 ⊢ (𝜑 → (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶))) ∈ 𝑈)
19	1, 7, 18	wunxp 9425	. 2 ⊢ (𝜑 → (((Base‘𝐷) ↑𝑚 (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶)))) ∈ 𝑈)
20		relfunc 16345	. . . 4 ⊢ Rel (𝐶 Func 𝐷)
21	20	a1i 11	. . 3 ⊢ (𝜑 → Rel (𝐶 Func 𝐷))
22		df-br 4584	. . . 4 ⊢ (𝑓(𝐶 Func 𝐷)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐶 Func 𝐷))
23		eqid 2610	. . . . . . . 8 ⊢ (Base‘𝐶) = (Base‘𝐶)
24		eqid 2610	. . . . . . . 8 ⊢ (Base‘𝐷) = (Base‘𝐷)
25		simpr 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓(𝐶 Func 𝐷)𝑔)
26	23, 24, 25	funcf1 16349	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓:(Base‘𝐶)⟶(Base‘𝐷))
27		fvex 6113	. . . . . . . 8 ⊢ (Base‘𝐷) ∈ V
28		fvex 6113	. . . . . . . 8 ⊢ (Base‘𝐶) ∈ V
29	27, 28	elmap 7772	. . . . . . 7 ⊢ (𝑓 ∈ ((Base‘𝐷) ↑𝑚 (Base‘𝐶)) ↔ 𝑓:(Base‘𝐶)⟶(Base‘𝐷))
30	26, 29	sylibr 223	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑓 ∈ ((Base‘𝐷) ↑𝑚 (Base‘𝐶)))
31		mapsspw 7779	. . . . . . . . . . 11 ⊢ (((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ⊆ 𝒫 (((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))))
32		fvssunirn 6127	. . . . . . . . . . . . 13 ⊢ ((Hom ‘𝐶)‘𝑧) ⊆ ∪ ran (Hom ‘𝐶)
33		ovssunirn 6579	. . . . . . . . . . . . 13 ⊢ ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ⊆ ∪ ran (Hom ‘𝐷)
34		xpss12 5148	. . . . . . . . . . . . 13 ⊢ ((((Hom ‘𝐶)‘𝑧) ⊆ ∪ ran (Hom ‘𝐶) ∧ ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ⊆ ∪ ran (Hom ‘𝐷)) → (((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)))
35	32, 33, 34	mp2an 704	. . . . . . . . . . . 12 ⊢ (((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷))
36		sspwb 4844	. . . . . . . . . . . 12 ⊢ ((((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↔ 𝒫 (((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)))
37	35, 36	mpbi 219	. . . . . . . . . . 11 ⊢ 𝒫 (((Hom ‘𝐶)‘𝑧) × ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷))
38	31, 37	sstri 3577	. . . . . . . . . 10 ⊢ (((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷))
39	38	rgenw 2908	. . . . . . . . 9 ⊢ ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷))
40		ss2ixp 7807	. . . . . . . . 9 ⊢ (∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ⊆ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) → X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ⊆ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)))
41	39, 40	ax-mp 5	. . . . . . . 8 ⊢ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ⊆ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷))
42	28, 28	xpex 6860	. . . . . . . . 9 ⊢ ((Base‘𝐶) × (Base‘𝐶)) ∈ V
43		fvex 6113	. . . . . . . . . . . . 13 ⊢ (Hom ‘𝐶) ∈ V
44	43	rnex 6992	. . . . . . . . . . . 12 ⊢ ran (Hom ‘𝐶) ∈ V
45	44	uniex 6851	. . . . . . . . . . 11 ⊢ ∪ ran (Hom ‘𝐶) ∈ V
46		fvex 6113	. . . . . . . . . . . . 13 ⊢ (Hom ‘𝐷) ∈ V
47	46	rnex 6992	. . . . . . . . . . . 12 ⊢ ran (Hom ‘𝐷) ∈ V
48	47	uniex 6851	. . . . . . . . . . 11 ⊢ ∪ ran (Hom ‘𝐷) ∈ V
49	45, 48	xpex 6860	. . . . . . . . . 10 ⊢ (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ∈ V
50	49	pwex 4774	. . . . . . . . 9 ⊢ 𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ∈ V
51	42, 50	ixpconst 7804	. . . . . . . 8 ⊢ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) = (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶)))
52	41, 51	sseqtri 3600	. . . . . . 7 ⊢ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)) ⊆ (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶)))
53		eqid 2610	. . . . . . . 8 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
54		eqid 2610	. . . . . . . 8 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
55	23, 53, 54, 25	funcixp 16350	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑔 ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐶)‘𝑧)))
56	52, 55	sseldi 3566	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → 𝑔 ∈ (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶))))
57		opelxpi 5072	. . . . . 6 ⊢ ((𝑓 ∈ ((Base‘𝐷) ↑𝑚 (Base‘𝐶)) ∧ 𝑔 ∈ (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶)))) → ⟨𝑓, 𝑔⟩ ∈ (((Base‘𝐷) ↑𝑚 (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶)))))
58	30, 56, 57	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑓(𝐶 Func 𝐷)𝑔) → ⟨𝑓, 𝑔⟩ ∈ (((Base‘𝐷) ↑𝑚 (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶)))))
59	58	ex 449	. . . 4 ⊢ (𝜑 → (𝑓(𝐶 Func 𝐷)𝑔 → ⟨𝑓, 𝑔⟩ ∈ (((Base‘𝐷) ↑𝑚 (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶))))))
60	22, 59	syl5bir 232	. . 3 ⊢ (𝜑 → (⟨𝑓, 𝑔⟩ ∈ (𝐶 Func 𝐷) → ⟨𝑓, 𝑔⟩ ∈ (((Base‘𝐷) ↑𝑚 (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶))))))
61	21, 60	relssdv 5135	. 2 ⊢ (𝜑 → (𝐶 Func 𝐷) ⊆ (((Base‘𝐷) ↑𝑚 (Base‘𝐶)) × (𝒫 (∪ ran (Hom ‘𝐶) × ∪ ran (Hom ‘𝐷)) ↑𝑚 ((Base‘𝐶) × (Base‘𝐶)))))
62	1, 19, 61	wunss 9413	1 ⊢ (𝜑 → (𝐶 Func 𝐷) ∈ 𝑈)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540  𝒫 cpw 4108  ⟨cop 4131  ∪ cuni 4372   class class class wbr 4583   × cxp 5036  ran crn 5039  Rel wrel 5043  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  1^st c1st 7057  2^nd c2nd 7058   ↑_𝑚 cmap 7744  Xcixp 7794  WUnicwun 9401  1c1 9816  4c4 10949  ;cdc 11369  Basecbs 15695  Hom chom 15779   Func cfunc 16337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-pm 7747  df-ixp 7795  df-wun 9403  df-slot 15699  df-base 15700  df-hom 15793  df-func 16341

This theorem is referenced by:  wunnat  16439  catcfuccl  16582