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 18022

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 2731	. . . . 5 ⊢ (𝑋 Func 𝑌) = (𝑋 Func 𝑌)
3		eqid 2731	. . . . 5 ⊢ (𝑋 Nat 𝑌) = (𝑋 Nat 𝑌)
4		eqid 2731	. . . . 5 ⊢ (Base‘𝑋) = (Base‘𝑋)
5		eqid 2731	. . . . 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 18005	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
11	6, 10	eleqtrd 2833	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat))
12	11	elin2d 4155	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ Cat)
13		catcfuccl.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
14	13, 10	eleqtrd 2833	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (𝑈 ∩ Cat))
15	14	elin2d 4155	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ Cat)
16		eqidd 2732	. . . . 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 17865	. . . 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 17120	. . . . . . 7 ⊢ Base = Slot (Base‘ndx)
19		catcfuccl.1	. . . . . . . 8 ⊢ (𝜑 → ω ∈ 𝑈)
20	9, 19	wunndx 17103	. . . . . . 7 ⊢ (𝜑 → ndx ∈ 𝑈)
21	18, 9, 20	wunstr 17096	. . . . . 6 ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈)
22	7, 8, 9, 6	catcbascl 18016	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
23	7, 8, 9, 13	catcbascl 18016	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑈)
24	9, 22, 23	wunfunc 17805	. . . . . 6 ⊢ (𝜑 → (𝑋 Func 𝑌) ∈ 𝑈)
25	9, 21, 24	wunop 10610	. . . . 5 ⊢ (𝜑 → ⟨(Base‘ndx), (𝑋 Func 𝑌)⟩ ∈ 𝑈)
26		homid 17313	. . . . . . 7 ⊢ Hom = Slot (Hom ‘ndx)
27	26, 9, 20	wunstr 17096	. . . . . 6 ⊢ (𝜑 → (Hom ‘ndx) ∈ 𝑈)
28	9, 22, 23	wunnat 17863	. . . . . 6 ⊢ (𝜑 → (𝑋 Nat 𝑌) ∈ 𝑈)
29	9, 27, 28	wunop 10610	. . . . 5 ⊢ (𝜑 → ⟨(Hom ‘ndx), (𝑋 Nat 𝑌)⟩ ∈ 𝑈)
30		ccoid 17315	. . . . . . 7 ⊢ comp = Slot (comp‘ndx)
31	30, 9, 20	wunstr 17096	. . . . . 6 ⊢ (𝜑 → (comp‘ndx) ∈ 𝑈)
32	9, 24, 24	wunxp 10612	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) ∈ 𝑈)
33	9, 32, 24	wunxp 10612	. . . . . . 7 ⊢ (𝜑 → (((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌)) ∈ 𝑈)
34	7, 8, 9, 13	catcccocl 18020	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (comp‘𝑌) ∈ 𝑈)
35	9, 34	wunrn 10617	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (comp‘𝑌) ∈ 𝑈)
36	9, 35	wununi 10594	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ ran (comp‘𝑌) ∈ 𝑈)
37	9, 36	wunrn 10617	. . . . . . . . . . 11 ⊢ (𝜑 → ran ∪ ran (comp‘𝑌) ∈ 𝑈)
38	9, 37	wununi 10594	. . . . . . . . . 10 ⊢ (𝜑 → ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈)
39	9, 38	wunpw 10595	. . . . . . . . 9 ⊢ (𝜑 → 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈)
40	7, 8, 9, 6	catcbaselcl 18018	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈)
41	9, 39, 40	wunmap 10614	. . . . . . . 8 ⊢ (𝜑 → (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ∈ 𝑈)
42	9, 28	wunrn 10617	. . . . . . . . . 10 ⊢ (𝜑 → ran (𝑋 Nat 𝑌) ∈ 𝑈)
43	9, 42	wununi 10594	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran (𝑋 Nat 𝑌) ∈ 𝑈)
44	9, 43, 43	wunxp 10612	. . . . . . . 8 ⊢ (𝜑 → (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)) ∈ 𝑈)
45	9, 41, 44	wunpm 10613	. . . . . . 7 ⊢ (𝜑 → ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ↑_pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌))) ∈ 𝑈)
46		fvex 6835	. . . . . . . . . . 11 ⊢ (1^st ‘𝑣) ∈ V
47		fvex 6835	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘𝑣) ∈ V
48		ovex 7379	. . . . . . . . . . . . . . . . 17 ⊢ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ∈ V
49		ovex 7379	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 Nat 𝑌) ∈ V
50	49	rnex 7840	. . . . . . . . . . . . . . . . . . 19 ⊢ ran (𝑋 Nat 𝑌) ∈ V
51	50	uniex 7674	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ran (𝑋 Nat 𝑌) ∈ V
52	51, 51	xpex 7686	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)) ∈ V
53		eqid 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))) = (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))
54		ovssunirn 7382	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))
55		ovssunirn 7382	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ∪ ran (comp‘𝑌)
56		rnss 5879	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ∪ ran (comp‘𝑌) → ran (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ran ∪ ran (comp‘𝑌))
57		uniss 4867	. . . . . . . . . . . . . . . . . . . . . . . . 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 3944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran ∪ ran (comp‘𝑌)
60		ovex 7379	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ V
61	60	elpw 4554	. . . . . . . . . . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . . . . . . . . . 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 7045	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))):(Base‘𝑋)⟶𝒫 ∪ ran ∪ ran (comp‘𝑌)
65		fvex 6835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (comp‘𝑌) ∈ V
66	65	rnex 7840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ran (comp‘𝑌) ∈ V
67	66	uniex 7674	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ ran (comp‘𝑌) ∈ V
68	67	rnex 7840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran ∪ ran (comp‘𝑌) ∈ V
69	68	uniex 7674	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ ran ∪ ran (comp‘𝑌) ∈ V
70	69	pwex 5318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ V
71		fvex 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑋) ∈ V
72	70, 71	elmap 8795	. . . . . . . . . . . . . . . . . . . 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 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋))
74	73	rgen2w 3052	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ)∀𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔)(𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋))
75		eqid 2731	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) = (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))
76	75	fmpo 8000	. . . . . . . . . . . . . . . . . 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 230	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))):((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋))
78		ovssunirn 7382	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔(𝑋 Nat 𝑌)ℎ) ⊆ ∪ ran (𝑋 Nat 𝑌)
79		ovssunirn 7382	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ∪ ran (𝑋 Nat 𝑌)
80		xpss12 5631	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔(𝑋 Nat 𝑌)ℎ) ⊆ ∪ ran (𝑋 Nat 𝑌) ∧ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ∪ ran (𝑋 Nat 𝑌)) → ((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)))
81	78, 79, 80	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌))
82		elpm2r 8769	. . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ↑_pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)))
84	83	sbcth 3756	. . . . . . . . . . . . . . 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 4366	. . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . 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 3756	. . . . . . . . . . . 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 4366	. . . . . . . . . . . 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 232	. . . . . . . . . . 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 3052	. . . . . . . . 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 2731	. . . . . . . . . 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 8000	. . . . . . . . 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 230	. . . . . . . 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 10615	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) ∈ 𝑈)
98	9, 31, 97	wunop 10610	. . . . 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 10599	. . . 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 2831	. . 3 ⊢ (𝜑 → 𝑄 ∈ 𝑈)
101	1, 12, 15	fuccat 17877	. . 3 ⊢ (𝜑 → 𝑄 ∈ Cat)
102	100, 101	elind 4150	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑈 ∩ Cat))
103	102, 10	eleqtrrd 2834	1 ⊢ (𝜑 → 𝑄 ∈ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2111 ∀wral 3047 Vcvv 3436 [wsbc 3741 ⦋csb 3850 ∩ cin 3901 ⊆ wss 3902 𝒫 cpw 4550 {ctp 4580 ⟨cop 4582 ∪ cuni 4859 ↦ cmpt 5172 × cxp 5614 ran crn 5617 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 ∈ cmpo 7348 ωcom 7796 1^st c1st 7919 2^nd c2nd 7920 ↑_m cmap 8750 ↑_pm cpm 8751 WUnicwun 10588 ndxcnx 17101 Basecbs 17117 Hom chom 17169 compcco 17170 Catccat 17567 Func cfunc 17758 Nat cnat 17848 FuncCat cfuc 17849 CatCatccatc 18002

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-inf2 9531 ax-cnex 11059 ax-resscn 11060 ax-1cn 11061 ax-icn 11062 ax-addcl 11063 ax-addrcl 11064 ax-mulcl 11065 ax-mulrcl 11066 ax-mulcom 11067 ax-addass 11068 ax-mulass 11069 ax-distr 11070 ax-i2m1 11071 ax-1ne0 11072 ax-1rid 11073 ax-rnegex 11074 ax-rrecex 11075 ax-cnre 11076 ax-pre-lttri 11077 ax-pre-lttrn 11078 ax-pre-ltadd 11079 ax-pre-mulgt0 11080

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-oadd 8389 df-omul 8390 df-er 8622 df-ec 8624 df-qs 8628 df-map 8752 df-pm 8753 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-wun 10590 df-ni 10760 df-pli 10761 df-mi 10762 df-lti 10763 df-plpq 10796 df-mpq 10797 df-ltpq 10798 df-enq 10799 df-nq 10800 df-erq 10801 df-plq 10802 df-mq 10803 df-1nq 10804 df-rq 10805 df-ltnq 10806 df-np 10869 df-plp 10871 df-ltp 10873 df-enr 10943 df-nr 10944 df-c 11009 df-pnf 11145 df-mnf 11146 df-xr 11147 df-ltxr 11148 df-le 11149 df-sub 11343 df-neg 11344 df-nn 12123 df-2 12185 df-3 12186 df-4 12187 df-5 12188 df-6 12189 df-7 12190 df-8 12191 df-9 12192 df-n0 12379 df-z 12466 df-dec 12586 df-uz 12730 df-fz 13405 df-struct 17055 df-slot 17090 df-ndx 17102 df-base 17118 df-hom 17182 df-cco 17183 df-cat 17571 df-cid 17572 df-func 17762 df-nat 17850 df-fuc 17851 df-catc 18003

This theorem is referenced by: (None)

W3C validator