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

Metamath Proof Explorer

Theorem exbaspos

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

Ref Expression
Assertion exbaspos ( 𝐵 ∈ 𝑉 → ∃ 𝑘 ∈ Poset 𝐵 = ( 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 3 resiposbas ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ } ) )
6 2 4 5 rspcedvdw ⊢ ( 𝐵 ∈ 𝑉 → ∃ 𝑘 ∈ Poset 𝐵 = ( Base ‘ 𝑘 ) )