Theorem termcterm2 49119

Description: A terminal object of the category of small categories is a terminal category. (Contributed by Zhi Wang, 18-Oct-2025.)

Hypotheses

Ref	Expression
termcterm.e	⊢ 𝐸 = (CatCat‘𝑈)
termcterm2.	⊢ (𝜑 → (𝑈 ∩ TermCat) ≠ ∅)
termcterm2.t	⊢ (𝜑 → 𝐶 ∈ (TermO‘𝐸))

Assertion

Ref	Expression
termcterm2	⊢ (𝜑 → 𝐶 ∈ TermCat)

Proof of Theorem termcterm2

Dummy variables 𝑑 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		termcterm2.	. . 3 ⊢ (𝜑 → (𝑈 ∩ TermCat) ≠ ∅)
2		n0 4352	. . 3 ⊢ ((𝑈 ∩ TermCat) ≠ ∅ ↔ ∃𝑑 𝑑 ∈ (𝑈 ∩ TermCat))
3	1, 2	sylib 218	. 2 ⊢ (𝜑 → ∃𝑑 𝑑 ∈ (𝑈 ∩ TermCat))
4		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑑 ∈ (𝑈 ∩ TermCat))
5	4	elin2d 4204	. . . . 5 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑑 ∈ TermCat)
6	5	termcthind 49098	. . . 4 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑑 ∈ ThinCat)
7		termcterm.e	. . . . 5 ⊢ 𝐸 = (CatCat‘𝑈)
8		eqid 2736	. . . . 5 ⊢ (Base‘𝐸) = (Base‘𝐸)
9		termcterm2.t	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (TermO‘𝐸))
10	9	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝐶 ∈ (TermO‘𝐸))
11		eqid 2736	. . . . . . . . 9 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
12		termorcl 18032	. . . . . . . . . 10 ⊢ (𝐶 ∈ (TermO‘𝐸) → 𝐸 ∈ Cat)
13	10, 12	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝐸 ∈ Cat)
14	8, 11, 13	istermoi 18041	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) ∧ 𝐶 ∈ (TermO‘𝐸)) → (𝐶 ∈ (Base‘𝐸) ∧ ∀𝑑 ∈ (Base‘𝐸)∃!𝑓 𝑓 ∈ (𝑑(Hom ‘𝐸)𝐶)))
15	10, 14	mpdan 687	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → (𝐶 ∈ (Base‘𝐸) ∧ ∀𝑑 ∈ (Base‘𝐸)∃!𝑓 𝑓 ∈ (𝑑(Hom ‘𝐸)𝐶)))
16	15	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝐶 ∈ (Base‘𝐸))
17	7, 8	elbasfv 17249	. . . . . 6 ⊢ (𝐶 ∈ (Base‘𝐸) → 𝑈 ∈ V)
18	16, 17	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑈 ∈ V)
19	4	elin1d 4203	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑑 ∈ 𝑈)
20	5	termccd 49099	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑑 ∈ Cat)
21	19, 20	elind 4199	. . . . . 6 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑑 ∈ (𝑈 ∩ Cat))
22	7, 8, 18	catcbas 18142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → (Base‘𝐸) = (𝑈 ∩ Cat))
23	21, 22	eleqtrrd 2843	. . . . 5 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑑 ∈ (Base‘𝐸))
24	7, 18, 19, 5	termcterm 49118	. . . . . 6 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝑑 ∈ (TermO‘𝐸))
25	13, 10, 24	termoeu1w 18060	. . . . 5 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝐶( ≃𝑐 ‘𝐸)𝑑)
26	7, 8, 18, 16, 23, 25	thincciso4 49079	. . . 4 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → (𝐶 ∈ ThinCat ↔ 𝑑 ∈ ThinCat))
27	6, 26	mpbird 257	. . 3 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝐶 ∈ ThinCat)
28	13, 10, 24	termoeu1 18059	. . . . . 6 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → ∃!𝑓 𝑓 ∈ (𝐶(Iso‘𝐸)𝑑))
29		euex 2576	. . . . . 6 ⊢ (∃!𝑓 𝑓 ∈ (𝐶(Iso‘𝐸)𝑑) → ∃𝑓 𝑓 ∈ (𝐶(Iso‘𝐸)𝑑))
30	28, 29	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → ∃𝑓 𝑓 ∈ (𝐶(Iso‘𝐸)𝑑))
31		eqid 2736	. . . . . . . 8 ⊢ (Base‘𝐶) = (Base‘𝐶)
32		eqid 2736	. . . . . . . 8 ⊢ (Base‘𝑑) = (Base‘𝑑)
33		eqid 2736	. . . . . . . 8 ⊢ (Iso‘𝐸) = (Iso‘𝐸)
34	7, 8, 31, 32, 18, 16, 23, 33	catciso 18152	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → (𝑓 ∈ (𝐶(Iso‘𝐸)𝑑) ↔ (𝑓 ∈ ((𝐶 Full 𝑑) ∩ (𝐶 Faith 𝑑)) ∧ (1st ‘𝑓):(Base‘𝐶)–1-1-onto→(Base‘𝑑))))
35	34	simplbda 499	. . . . . 6 ⊢ (((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) ∧ 𝑓 ∈ (𝐶(Iso‘𝐸)𝑑)) → (1st ‘𝑓):(Base‘𝐶)–1-1-onto→(Base‘𝑑))
36		fvex 6917	. . . . . . 7 ⊢ (Base‘𝐶) ∈ V
37	36	f1oen 9009	. . . . . 6 ⊢ ((1st ‘𝑓):(Base‘𝐶)–1-1-onto→(Base‘𝑑) → (Base‘𝐶) ≈ (Base‘𝑑))
38	35, 37	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) ∧ 𝑓 ∈ (𝐶(Iso‘𝐸)𝑑)) → (Base‘𝐶) ≈ (Base‘𝑑))
39	30, 38	exlimddv 1935	. . . 4 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → (Base‘𝐶) ≈ (Base‘𝑑))
40	32	istermc3 49096	. . . . . 6 ⊢ (𝑑 ∈ TermCat ↔ (𝑑 ∈ ThinCat ∧ (Base‘𝑑) ≈ 1o))
41	5, 40	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → (𝑑 ∈ ThinCat ∧ (Base‘𝑑) ≈ 1o))
42	41	simprd 495	. . . 4 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → (Base‘𝑑) ≈ 1o)
43		entr 9042	. . . 4 ⊢ (((Base‘𝐶) ≈ (Base‘𝑑) ∧ (Base‘𝑑) ≈ 1o) → (Base‘𝐶) ≈ 1o)
44	39, 42, 43	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → (Base‘𝐶) ≈ 1o)
45	31	istermc3 49096	. . 3 ⊢ (𝐶 ∈ TermCat ↔ (𝐶 ∈ ThinCat ∧ (Base‘𝐶) ≈ 1o))
46	27, 44, 45	sylanbrc 583	. 2 ⊢ ((𝜑 ∧ 𝑑 ∈ (𝑈 ∩ TermCat)) → 𝐶 ∈ TermCat)
47	3, 46	exlimddv 1935	1 ⊢ (𝜑 → 𝐶 ∈ TermCat)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∃!weu 2567   ≠ wne 2939  ∀wral 3060  Vcvv 3479   ∩ cin 3949  ∅c0 4332   class class class wbr 5141  –1-1-onto→wf1o 6558  ‘cfv 6559  (class class class)co 7429  1^st c1st 8008  1_oc1o 8495   ≈ cen 8978  Basecbs 17243  Hom chom 17304  Catccat 17703  Isociso 17786   Full cful 17945   Faith cfth 17946  TermOctermo 18023  CatCatccatc 18139  ThinCatcthinc 49040  TermCatctermc 49092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751  ax-cnex 11207  ax-resscn 11208  ax-1cn 11209  ax-icn 11210  ax-addcl 11211  ax-addrcl 11212  ax-mulcl 11213  ax-mulrcl 11214  ax-mulcom 11215  ax-addass 11216  ax-mulass 11217  ax-distr 11218  ax-i2m1 11219  ax-1ne0 11220  ax-1rid 11221  ax-rnegex 11222  ax-rrecex 11223  ax-cnre 11224  ax-pre-lttri 11225  ax-pre-lttrn 11226  ax-pre-ltadd 11227  ax-pre-mulgt0 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4906  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-om 7884  df-1st 8010  df-2nd 8011  df-supp 8182  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-1o 8502  df-er 8741  df-map 8864  df-ixp 8934  df-en 8982  df-dom 8983  df-sdom 8984  df-fin 8985  df-pnf 11293  df-mnf 11294  df-xr 11295  df-ltxr 11296  df-le 11297  df-sub 11490  df-neg 11491  df-nn 12263  df-2 12325  df-3 12326  df-4 12327  df-5 12328  df-6 12329  df-7 12330  df-8 12331  df-9 12332  df-n0 12523  df-z 12610  df-dec 12730  df-uz 12875  df-fz 13544  df-struct 17180  df-slot 17215  df-ndx 17227  df-base 17244  df-hom 17317  df-cco 17318  df-cat 17707  df-cid 17708  df-sect 17787  df-inv 17788  df-iso 17789  df-cic 17836  df-func 17899  df-idfu 17900  df-cofu 17901  df-full 17947  df-fth 17948  df-termo 18026  df-catc 18140  df-thinc 49041  df-termc 49093

This theorem is referenced by:  termcterm3  49120  termc2  49121