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→ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } }