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 ( Base ↾ TermCat ) : TermCat –onto→ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } }

Proof

Step Hyp Ref Expression
1 basfn ⊢ Base Fn V
2 id ⊢ ( 𝑐 ∈ TermCat → 𝑐 ∈ TermCat )
3 eqid ⊢ ( Base ‘ 𝑐 ) = ( Base ‘ 𝑐 )
4 2 3 termcbas ⊢ ( 𝑐 ∈ TermCat → ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } )
5 discsntermlem ⊢ ( ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } → ( Base ‘ 𝑐 ) ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } )
6 4 5 syl ⊢ ( 𝑐 ∈ TermCat → ( Base ‘ 𝑐 ) ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } )
7 basrestermcfolem ⊢ ( 𝑎 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } → ∃ 𝑥 𝑎 = { 𝑥 } )
8 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑎 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑎 ) ⟩ }
9 eqid ⊢ ( ProsetToCat ‘ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑎 ) ⟩ } ) = ( ProsetToCat ‘ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑎 ) ⟩ } )
10 8 9 discsnterm ⊢ ( ∃ 𝑥 𝑎 = { 𝑥 } → ( ProsetToCat ‘ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑎 ) ⟩ } ) ∈ TermCat )
11 7 10 syl ⊢ ( 𝑎 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } → ( ProsetToCat ‘ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑎 ) ⟩ } ) ∈ TermCat )
12 8 9 discbas ⊢ ( 𝑎 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } → 𝑎 = ( Base ‘ ( ProsetToCat ‘ { ⟨ ( Base ‘ ndx ) , 𝑎 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑎 ) ⟩ } ) ) )
13 1 6 11 12 slotresfo ⊢ ( Base ↾ TermCat ) : TermCat –onto→ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } }