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