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 18211

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 2762	. . . . 5 ⊢ (𝑋 Func 𝑌) = (𝑋 Func 𝑌)
3		eqid 2762	. . . . 5 ⊢ (𝑋 Nat 𝑌) = (𝑋 Nat 𝑌)
4		eqid 2762	. . . . 5 ⊢ (Base‘𝑋) = (Base‘𝑋)
5		eqid 2762	. . . . 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 18194	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
11	6, 10	eleqtrd 2864	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat))
12	11	elin2d 4154	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ Cat)
13		catcfuccl.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
14	13, 10	eleqtrd 2864	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (𝑈 ∩ Cat))
15	14	elin2d 4154	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ Cat)
16		eqidd 2763	. . . . 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 18054	. . . 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 17308	. . . . . . 7 ⊢ Base = Slot (Base‘ndx)
19		catcfuccl.1	. . . . . . . 8 ⊢ (𝜑 → ω ∈ 𝑈)
20	9, 19	wunndx 17291	. . . . . . 7 ⊢ (𝜑 → ndx ∈ 𝑈)
21	18, 9, 20	wunstr 17284	. . . . . 6 ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈)
22	7, 8, 9, 6	catcbascl 18205	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
23	7, 8, 9, 13	catcbascl 18205	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑈)
24	9, 22, 23	wunfunc 17994	. . . . . 6 ⊢ (𝜑 → (𝑋 Func 𝑌) ∈ 𝑈)
25	9, 21, 24	wunop 10734	. . . . 5 ⊢ (𝜑 → ⟨(Base‘ndx), (𝑋 Func 𝑌)⟩ ∈ 𝑈)
26		homid 17501	. . . . . . 7 ⊢ Hom = Slot (Hom ‘ndx)
27	26, 9, 20	wunstr 17284	. . . . . 6 ⊢ (𝜑 → (Hom ‘ndx) ∈ 𝑈)
28	9, 22, 23	wunnat 18052	. . . . . 6 ⊢ (𝜑 → (𝑋 Nat 𝑌) ∈ 𝑈)
29	9, 27, 28	wunop 10734	. . . . 5 ⊢ (𝜑 → ⟨(Hom ‘ndx), (𝑋 Nat 𝑌)⟩ ∈ 𝑈)
30		ccoid 17503	. . . . . . 7 ⊢ comp = Slot (comp‘ndx)
31	30, 9, 20	wunstr 17284	. . . . . 6 ⊢ (𝜑 → (comp‘ndx) ∈ 𝑈)
32	9, 24, 24	wunxp 10736	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) ∈ 𝑈)
33	9, 32, 24	wunxp 10736	. . . . . . 7 ⊢ (𝜑 → (((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌)) ∈ 𝑈)
34	7, 8, 9, 13	catcccocl 18209	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (comp‘𝑌) ∈ 𝑈)
35	9, 34	wunrn 10741	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (comp‘𝑌) ∈ 𝑈)
36	9, 35	wununi 10718	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ ran (comp‘𝑌) ∈ 𝑈)
37	9, 36	wunrn 10741	. . . . . . . . . . 11 ⊢ (𝜑 → ran ∪ ran (comp‘𝑌) ∈ 𝑈)
38	9, 37	wununi 10718	. . . . . . . . . 10 ⊢ (𝜑 → ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈)
39	9, 38	wunpw 10719	. . . . . . . . 9 ⊢ (𝜑 → 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈)
40	7, 8, 9, 6	catcbaselcl 18207	. . . . . . . . 9 ⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈)
41	9, 39, 40	wunmap 10738	. . . . . . . 8 ⊢ (𝜑 → (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ∈ 𝑈)
42	9, 28	wunrn 10741	. . . . . . . . . 10 ⊢ (𝜑 → ran (𝑋 Nat 𝑌) ∈ 𝑈)
43	9, 42	wununi 10718	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran (𝑋 Nat 𝑌) ∈ 𝑈)
44	9, 43, 43	wunxp 10736	. . . . . . . 8 ⊢ (𝜑 → (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)) ∈ 𝑈)
45	9, 41, 44	wunpm 10737	. . . . . . 7 ⊢ (𝜑 → ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ↑_pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌))) ∈ 𝑈)
46		fvex 6895	. . . . . . . . . . 11 ⊢ (1^st ‘𝑣) ∈ V
47		fvex 6895	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘𝑣) ∈ V
48		ovex 7449	. . . . . . . . . . . . . . . . 17 ⊢ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ∈ V
49		ovex 7449	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 Nat 𝑌) ∈ V
50	49	rnex 7910	. . . . . . . . . . . . . . . . . . 19 ⊢ ran (𝑋 Nat 𝑌) ∈ V
51	50	uniex 7746	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ ran (𝑋 Nat 𝑌) ∈ V
52	51, 51	xpex 7755	. . . . . . . . . . . . . . . . 17 ⊢ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)) ∈ V
53		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))) = (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))
54		ovssunirn 7452	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))
55		ovssunirn 7452	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ∪ ran (comp‘𝑌)
56		rnss 5927	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ∪ ran (comp‘𝑌) → ran (⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥)) ⊆ ran ∪ ran (comp‘𝑌))
57		uniss 4878	. . . . . . . . . . . . . . . . . . . . . . . . 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 3943	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran ∪ ran (comp‘𝑌)
60		ovex 7449	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ V
61	60	elpw 4564	. . . . . . . . . . . . . . . . . . . . . . 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 7108	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))):(Base‘𝑋)⟶𝒫 ∪ ran ∪ ran (comp‘𝑌)
65		fvex 6895	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (comp‘𝑌) ∈ V
66	65	rnex 7910	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ran (comp‘𝑌) ∈ V
67	66	uniex 7746	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∪ ran (comp‘𝑌) ∈ V
68	67	rnex 7910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ran ∪ ran (comp‘𝑌) ∈ V
69	68	uniex 7746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ ran ∪ ran (comp‘𝑌) ∈ V
70	69	pwex 5349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ V
71		fvex 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑋) ∈ V
72	70, 71	elmap 8881	. . . . . . . . . . . . . . . . . . . 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 3083	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ)∀𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔)(𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋))
75		eqid 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) = (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))
76	75	fmpo 8068	. . . . . . . . . . . . . . . . . 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 7452	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔(𝑋 Nat 𝑌)ℎ) ⊆ ∪ ran (𝑋 Nat 𝑌)
79		ovssunirn 7452	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ∪ ran (𝑋 Nat 𝑌)
80		xpss12 5674	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑔(𝑋 Nat 𝑌)ℎ) ⊆ ∪ ran (𝑋 Nat 𝑌) ∧ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ∪ ran (𝑋 Nat 𝑌)) → ((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)))
81	78, 79, 80	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌))
82		elpm2r 8847	. . . . . . . . . . . . . . . . 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 706	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑_m (Base‘𝑋)) ↑_pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran (𝑋 Nat 𝑌)))
84	83	sbcth 3757	. . . . . . . . . . . . . . 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 4377	. . . . . . . . . . . . . . 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 3757	. . . . . . . . . . . 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 4377	. . . . . . . . . . . 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 3083	. . . . . . . . 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 2762	. . . . . . . . . 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 8068	. . . . . . . . 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 10739	. . . . . 6 ⊢ (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩(comp‘𝑌)((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) ∈ 𝑈)
98	9, 31, 97	wunop 10734	. . . . 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 10723	. . . 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 2862	. . 3 ⊢ (𝜑 → 𝑄 ∈ 𝑈)
101	1, 12, 15	fuccat 18066	. . 3 ⊢ (𝜑 → 𝑄 ∈ Cat)
102	100, 101	elind 4149	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑈 ∩ Cat))
103	102, 10	eleqtrrd 2865	1 ⊢ (𝜑 → 𝑄 ∈ 𝐵)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2145 ∀wral 3078 Vcvv 3453 [wsbc 3742 ⦋csb 3850 ∩ cin 3901 ⊆ wss 3902 𝒫 cpw 4560 {ctp 4591 ⟨cop 4593 ∪ cuni 4870 ↦ cmpt 5190 × cxp 5657 ran crn 5660 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 ∈ cmpo 7418 ωcom 7865 1^st c1st 7987 2^nd c2nd 7988 ↑_m cmap 8829 ↑_pm cpm 8830 WUnicwun 10712 ndxcnx 17289 Basecbs 17305 Hom chom 17357 compcco 17358 Catccat 17756 Func cfunc 17947 Nat cnat 18037 FuncCat cfuc 18038 CatCatccatc 18191

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-oadd 8462 df-omul 8463 df-er 8699 df-ec 8701 df-qs 8705 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-wun 10714 df-ni 10884 df-pli 10885 df-mi 10886 df-lti 10887 df-plpq 10920 df-mpq 10921 df-ltpq 10922 df-enq 10923 df-nq 10924 df-erq 10925 df-plq 10926 df-mq 10927 df-1nq 10928 df-rq 10929 df-ltnq 10930 df-np 10993 df-plp 10995 df-ltp 10997 df-enr 11067 df-nr 11068 df-c 11133 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-fz 13564 df-struct 17243 df-slot 17278 df-ndx 17290 df-base 17306 df-hom 17370 df-cco 17371 df-cat 17760 df-cid 17761 df-func 17951 df-nat 18039 df-fuc 18040 df-catc 18192

This theorem is used by: (None)

W3C validator