catcfuccl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > catcfuccl		Structured version Visualization version GIF version

Theorem catcfuccl 18165

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.)

**Hypotheses**
Ref	Expression
catcfuccl.c	⊢ 𝐶 = (CatCat‘𝑈)
catcfuccl.b	⊢ 𝐵 = (Base‘𝐶)
catcfuccl.o	⊢ 𝑄 = (𝑋 FuncCat 𝑌)
catcfuccl.u	⊢ (𝜑 → 𝑈 ∈ WUni)
catcfuccl.1	⊢ (𝜑 → ω ∈ 𝑈)
catcfuccl.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
catcfuccl.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)

**Assertion**
Ref	Expression
catcfuccl	⊢ (𝜑 → 𝑄 ∈ 𝐵)

Proof of Theorem catcfuccl Dummy variables 𝑎 𝑏 𝑓 𝑔 ℎ 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		catcfuccl.o	. . . . 5 ⊢ 𝑄 = (𝑋 FuncCat 𝑌)
2		eqid 2765	. . . . 5 ⊢ (𝑋 Func 𝑌) = (𝑋 Func 𝑌)
3		eqid 2765	. . . . 5 ⊢ (𝑋 Nat 𝑌) = (𝑋 Nat 𝑌)
4		eqid 2765	. . . . 5 ⊢ (Base‘𝑋) = (Base‘𝑋)
5		eqid 2765	. . . . 5 ⊢ (comp‘𝑌) = (comp‘𝑌)
6		catcfuccl.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
7		catcfuccl.c	. . . . . . . 8 ⊢ 𝐶 = (CatCat‘𝑈)
8		catcfuccl.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐶)
9		catcfuccl.u	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ WUni)
10	7, 8, 9	catcbas 18148	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
11	6, 10	eleqtrd 2867	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat))
12	11	elin2d 4160	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ Cat)
13		catcfuccl.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
14	13, 10	eleqtrd 2867	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (𝑈 ∩ Cat))
15	14	elin2d 4160	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ Cat)
16		eqidd 2766	. . . . 5 ⊢ (𝜑 → (𝑣 ∈ ((𝑋 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 ‘ℎ)‘𝑥))(𝑎‘𝑥))))))
17	1, 2, 3, 4, 5, 12, 15, 16	fucval 18008	. . . 4 ⊢ (𝜑 → 𝑄 = {⟨(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 ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩})
18		baseid 17262	. . . . . . 7 ⊢ Base = Slot (Base‘ndx)
19		catcfuccl.1	. . . . . . . 8 ⊢ (𝜑 → ω ∈ 𝑈)
20	9, 19	wunndx 17245	. . . . . . 7 ⊢ (𝜑 → ndx ∈ 𝑈)
21	18, 9, 20	wunstr 17238	. . . . . 6 ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈)
22	7, 8, 9, 6	catcbascl 18159	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
23	7, 8, 9, 13	catcbascl 18159	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑈)
24	9, 22, 23	wunfunc 17948	. . . . . 6 ⊢ (𝜑 → (𝑋 Func 𝑌) ∈ 𝑈)
25	9, 21, 24	wunop 10695	. . . . 5 ⊢ (𝜑 → ⟨(Base‘ndx), (𝑋 Func 𝑌)⟩ ∈ 𝑈)
26		homid 17455	. . . . . . 7 ⊢ Hom = Slot (Hom ‘ndx)
27	26, 9, 20	wunstr 17238	. . . . . 6 ⊢ (𝜑 → (Hom ‘ndx) ∈ 𝑈)
28	9, 22, 23	wunnat 18006	. . . . . 6 ⊢ (𝜑 → (𝑋 Nat 𝑌) ∈ 𝑈)
29	9, 27, 28	wunop 10695	. . . . 5 ⊢ (𝜑 → ⟨(Hom ‘ndx), (𝑋 Nat 𝑌)⟩ ∈ 𝑈)
30		ccoid 17457	. . . . . . 7 ⊢ comp = Slot (comp‘ndx)
31	30, 9, 20	wunstr 17238	. . . . . 6 ⊢ (𝜑 → (comp‘ndx) ∈ 𝑈)
32	9, 24, 24	wunxp 10697	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) ∈ 𝑈)
33	9, 32, 24	wunxp 10697	. . . . . . 7 ⊢ (𝜑 → (((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌)) ∈ 𝑈)
34	7, 8, 9, 13	catcccocl 18163	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (comp‘𝑌) ∈ 𝑈)
35	9, 34	wunrn 10702	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (comp‘𝑌) ∈ 𝑈)
36	9, 35	wununi 10679	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ ran (comp‘𝑌) ∈ 𝑈)
37	9, 36	wunrn 10702	. . . . . . . . . . 11 ⊢ (𝜑 → ran ∪ ran (comp‘𝑌) ∈ 𝑈)
38	9, 37	wununi 10679	. . . . . . . . . 10 ⊢ (𝜑 → ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈)
39	9, 38	wunpw 10680	. . . . . . . . 9 ⊢ (𝜑 → 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈)
40	7, 8, 9, 6	catcbaselcl 18161	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈)
41	9, 39, 40	wunmap 10699	. . . . . . . 8 ⊢ (𝜑 → (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ∈ 𝑈)
42	9, 28	wunrn 10702	. . . . . . . . . 10 ⊢ (𝜑 → ran (𝑋 Nat 𝑌) ∈ 𝑈)
43	9, 42	wununi 10679	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran (𝑋 Nat 𝑌) ∈ 𝑈)
44	9, 43, 43	wunxp 10697	. . . . . . . 8 ⊢ (𝜑 → (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)) ∈ 𝑈)
45	9, 41, 44	wunpm 10698	. . . . . . 7 ⊢ (𝜑 → ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ↑_pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌))) ∈ 𝑈)
46		fvex 6884	. . . . . . . . . . 11 ⊢ (1^st ‘𝑣) ∈ V
47		fvex 6884	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘𝑣) ∈ V
48		ovex 7433	. . . . . . . . . . . . . . . . 17 ⊢ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ∈ V
49		ovex 7433	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 Nat 𝑌) ∈ V
50	49	rnex 7895	. . . . . . . . . . . . . . . . . . 19 ⊢ ran (𝑋 Nat 𝑌) ∈ V
51	50	uniex 7728	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ran (𝑋 Nat 𝑌) ∈ V
52	51, 51	xpex 7740	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)) ∈ V
53		eqid 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))) = (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))
54		ovssunirn 7436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))
55		ovssunirn 7436	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ∪ ran (comp‘𝑌)
56		rnss 5920	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ∪ ran (comp‘𝑌) → ran (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ran ∪ ran (comp‘𝑌))
57		uniss 4876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (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 10	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ ran (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ∪ ran ∪ ran (comp‘𝑌)
59	54, 58	sstri 3948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran ∪ ran (comp‘𝑌)
60		ovex 7433	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ V
61	60	elpw 4562	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌) ↔ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran ∪ ran (comp‘𝑌))
62	59, 61	mpbir 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌)
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (Base‘𝑋) → ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌))
64	53, 63	fmpti 7097	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))):(Base‘𝑋)⟶𝒫 ∪ ran ∪ ran (comp‘𝑌)
65		fvex 6884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (comp‘𝑌) ∈ V
66	65	rnex 7895	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ran (comp‘𝑌) ∈ V
67	66	uniex 7728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ ran (comp‘𝑌) ∈ V
68	67	rnex 7895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran ∪ ran (comp‘𝑌) ∈ V
69	68	uniex 7728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ ran ∪ ran (comp‘𝑌) ∈ V
70	69	pwex 5342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ V
71		fvex 6884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑋) ∈ V
72	70, 71	elmap 8857	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (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 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋))
74	73	rgen2w 3084	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ)∀𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔)(𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋))
75		eqid 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) = (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))
76	75	fmpo 8053	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑏 ∈ (𝑔(𝑋 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 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))):((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋))
78		ovssunirn 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔(𝑋 Nat 𝑌)ℎ) ⊆ ∪ ran (𝑋 Nat 𝑌)
79		ovssunirn 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ∪ ran (𝑋 Nat 𝑌)
80		xpss12 5667	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔(𝑋 Nat 𝑌)ℎ) ⊆ ∪ ran (𝑋 Nat 𝑌) ∧ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ∪ ran (𝑋 Nat 𝑌)) → ((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)))
81	78, 79, 80	mp2an 704	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌))
82		elpm2r 8830	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝒫 ∪ 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 705	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ↑_pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)))
84	83	sbcth 3762	. . . . . . . . . . . . . . 15 ⊢ ((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 4373	. . . . . . . . . . . . . . 15 ⊢ ((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 235	. . . . . . . . . . . . . 14 ⊢ ((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 5	. . . . . . . . . . . . 13 ⊢ ⦋(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 3762	. . . . . . . . . . . 12 ⊢ ((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 4373	. . . . . . . . . . . 12 ⊢ ((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 235	. . . . . . . . . . 11 ⊢ ((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 5	. . . . . . . . . 10 ⊢ ⦋(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 3084	. . . . . . . . 9 ⊢ ∀𝑣 ∈ ((𝑋 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 2765	. . . . . . . . . 10 ⊢ (𝑣 ∈ ((𝑋 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 8053	. . . . . . . . 9 ⊢ (∀𝑣 ∈ ((𝑋 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 233	. . . . . . . 8 ⊢ (𝑣 ∈ ((𝑋 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 11	. . . . . . 7 ⊢ (𝜑 → (𝑣 ∈ ((𝑋 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	9, 33, 45, 96	wunf 10700	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) ∈ 𝑈)
98	9, 31, 97	wunop 10695	. . . . 5 ⊢ (𝜑 → ⟨(comp‘ndx), (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩ ∈ 𝑈)
99	9, 25, 29, 98	wuntp 10684	. . . 4 ⊢ (𝜑 → {⟨(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	17, 99	eqeltrd 2865	. . 3 ⊢ (𝜑 → 𝑄 ∈ 𝑈)
101	1, 12, 15	fuccat 18020	. . 3 ⊢ (𝜑 → 𝑄 ∈ Cat)
102	100, 101	elind 4155	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑈 ∩ Cat))
103	102, 10	eleqtrrd 2868	1 ⊢ (𝜑 → 𝑄 ∈ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1563 ∈ wcel 2145 ∀wral 3079 Vcvv 3457 [wsbc 3747 ⦋csb 3855 ∩ cin 3906 ⊆ wss 3907 𝒫 cpw 4558 {ctp 4589 ⟨cop 4591 ∪ cuni 4868 ↦ cmpt 5186 × cxp 5650 ran crn 5653 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ∈ cmpo 7402 ωcom 7850 1^st c1st 7972 2^nd c2nd 7973 ↑_m cmap 8812 ↑_pm cpm 8813 WUnicwun 10673 ndxcnx 17243 Basecbs 17259 Hom chom 17311 compcco 17312 Catccat 17710 Func cfunc 17901 Nat cnat 17991 FuncCat cfuc 17992 CatCatccatc 18145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-inf2 9598 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-oadd 8445 df-omul 8446 df-er 8682 df-ec 8684 df-qs 8688 df-map 8814 df-pm 8815 df-ixp 8884 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-wun 10675 df-ni 10845 df-pli 10846 df-mi 10847 df-lti 10848 df-plpq 10881 df-mpq 10882 df-ltpq 10883 df-enq 10884 df-nq 10885 df-erq 10886 df-plq 10887 df-mq 10888 df-1nq 10889 df-rq 10890 df-ltnq 10891 df-np 10954 df-plp 10956 df-ltp 10958 df-enr 11028 df-nr 11029 df-c 11094 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-9 12301 df-n0 12496 df-z 12583 df-dec 12703 df-uz 12854 df-fz 13527 df-struct 17197 df-slot 17232 df-ndx 17244 df-base 17260 df-hom 17324 df-cco 17325 df-cat 17714 df-cid 17715 df-func 17905 df-nat 17993 df-fuc 17994 df-catc 18146

This theorem is referenced by: (None)

W3C validator