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 ‘ 𝑘 ) )