Theorem basresprsfo

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

	Ref	Expression
Assertion	basresprsfo	⊢ ( Base ↾ Proset ) : Proset –onto→ V

Proof

Step	Hyp	Ref	Expression
1		basfn	⊢ Base Fn V
2		fvexd	⊢ ( 𝑘 ∈ Proset → ( Base ‘ 𝑘 ) ∈ V )
3		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑏 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑏 ) ⟩ }
4	3	resipos	⊢ ( 𝑏 ∈ V → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑏 ) ⟩ } ∈ Poset )
5		posprs	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑏 ) ⟩ } ∈ Poset → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑏 ) ⟩ } ∈ Proset )
6	4 5	syl	⊢ ( 𝑏 ∈ V → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑏 ) ⟩ } ∈ Proset )
7	3	resiposbas	⊢ ( 𝑏 ∈ V → 𝑏 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝑏 ) ⟩ } ) )
8	1 2 6 7	slotresfo	⊢ ( Base ↾ Proset ) : Proset –onto→ V