This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem basrestermcfo

Description: The base function restricted to the class of terminal categories maps the class of terminal categories onto the class of singletons. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Assertion basrestermcfo Could not format assertion : No typesetting found for |- ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } } with typecode |-

Proof

Step Hyp Ref Expression
1 basfn ⊢ Base Fn V
2 id Could not format ( c e. TermCat -> c e. TermCat ) : No typesetting found for |- ( c e. TermCat -> c e. TermCat ) with typecode |-
3 eqid ⊢ Base c = Base c
4 2 3 termcbas Could not format ( c e. TermCat -> E. x ( Base ` c ) = { x } ) : No typesetting found for |- ( c e. TermCat -> E. x ( Base ` c ) = { x } ) with typecode |-
5 discsntermlem ⊢ ∃ x Base c = x → Base c ∈ b | ∃ x b = x
6 4 5 syl Could not format ( c e. TermCat -> ( Base ` c ) e. { b | E. x b = { x } } ) : No typesetting found for |- ( c e. TermCat -> ( Base ` c ) e. { b | E. x b = { x } } ) with typecode |-
7 basrestermcfolem ⊢ a ∈ b | ∃ x b = x → ∃ x a = x
8 eqid ⊢ Base ndx a ≤ ndx I ↾ a = Base ndx a ≤ ndx I ↾ a
9 eqid ⊢ ProsetToCat ⁡ Base ndx a ≤ ndx I ↾ a = ProsetToCat ⁡ Base ndx a ≤ ndx I ↾ a
10 8 9 discsnterm Could not format ( E. x a = { x } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat ) : No typesetting found for |- ( E. x a = { x } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat ) with typecode |-
11 7 10 syl Could not format ( a e. { b | E. x b = { x } } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat ) : No typesetting found for |- ( a e. { b | E. x b = { x } } -> ( ProsetToCat ` { <. ( Base ` ndx ) , a >. , <. ( le ` ndx ) , ( _I |` a ) >. } ) e. TermCat ) with typecode |-
12 8 9 discbas ⊢ a ∈ b | ∃ x b = x → a = Base ProsetToCat ⁡ Base ndx a ≤ ndx I ↾ a
13 1 6 11 12 slotresfo Could not format ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } } : No typesetting found for |- ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } } with typecode |-