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 ( 𝐵 ∈ 𝑉 → ∃ 𝑘 ∈ Proset 𝐵 = ( Base ‘ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑘 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } → ( Base ‘ 𝑘 ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } ) )
2 1 eqeq2d ⊢ ( 𝑘 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } → ( 𝐵 = ( Base ‘ 𝑘 ) ↔ 𝐵 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } ) ) )
3 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
4 3 resipos ⊢ ( 𝐵 ∈ 𝑉 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } ∈ Poset )
5 posprs ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } ∈ Poset → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } ∈ Proset )
6 4 5 syl ⊢ ( 𝐵 ∈ 𝑉 → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } ∈ Proset )
7 3 resiposbas ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } ) )
8 2 6 7 rspcedvdw ⊢ ( 𝐵 ∈ 𝑉 → ∃ 𝑘 ∈ Proset 𝐵 = ( Base ‘ 𝑘 ) )