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

Metamath Proof Explorer

Theorem exbasprs

Description: There exists a preordered set for any base set. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Assertion exbasprs ⊢ B ∈ V → ∃ k ∈ Proset B = Base k

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ k = Base ndx B ≤ ndx I ↾ B → Base k = Base Base ndx B ≤ ndx I ↾ B
2 1 eqeq2d ⊢ k = Base ndx B ≤ ndx I ↾ B → B = Base k ↔ B = Base Base ndx B ≤ ndx I ↾ B
3 eqid ⊢ Base ndx B ≤ ndx I ↾ B = Base ndx B ≤ ndx I ↾ B
4 3 resipos ⊢ B ∈ V → Base ndx B ≤ ndx I ↾ B ∈ Poset
5 posprs ⊢ Base ndx B ≤ ndx I ↾ B ∈ Poset → Base ndx B ≤ ndx I ↾ B ∈ Proset
6 4 5 syl ⊢ B ∈ V → Base ndx B ≤ ndx I ↾ B ∈ Proset
7 3 resiposbas ⊢ B ∈ V → B = Base Base ndx B ≤ ndx I ↾ B
8 2 6 7 rspcedvdw ⊢ B ∈ V → ∃ k ∈ Proset B = Base k