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

Metamath Proof Explorer

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