Theorem basresposfo

Description: The base function restricted to the class of posets maps the class of posets onto the universal class. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Assertion	basresposfo	⊢ ( Base ↾ Poset ) : Poset –onto→ V

Proof

Step	Hyp	Ref	Expression
1		basfn	⊢ Base Fn V
2		ssv	⊢ Poset ⊆ V
3		fnssres	⊢ ( ( Base Fn V ∧ Poset ⊆ V ) → ( Base ↾ Poset ) Fn Poset )
4	1 2 3	mp2an	⊢ ( Base ↾ Poset ) Fn Poset
5		dffn2	⊢ ( ( Base ↾ Poset ) Fn Poset ↔ ( Base ↾ Poset ) : Poset ⟶ V )
6	4 5	mpbi	⊢ ( Base ↾ Poset ) : Poset ⟶ V
7		exbaspos	⊢ ( 𝑏 ∈ V → ∃ 𝑘 ∈ Poset 𝑏 = ( Base ‘ 𝑘 ) )
8		fvres	⊢ ( 𝑘 ∈ Poset → ( ( Base ↾ Poset ) ‘ 𝑘 ) = ( Base ‘ 𝑘 ) )
9	8	eqeq2d	⊢ ( 𝑘 ∈ Poset → ( 𝑏 = ( ( Base ↾ Poset ) ‘ 𝑘 ) ↔ 𝑏 = ( Base ‘ 𝑘 ) ) )
10	9	rexbiia	⊢ ( ∃ 𝑘 ∈ Poset 𝑏 = ( ( Base ↾ Poset ) ‘ 𝑘 ) ↔ ∃ 𝑘 ∈ Poset 𝑏 = ( Base ‘ 𝑘 ) )
11	7 10	sylibr	⊢ ( 𝑏 ∈ V → ∃ 𝑘 ∈ Poset 𝑏 = ( ( Base ↾ Poset ) ‘ 𝑘 ) )
12	11	rgen	⊢ ∀ 𝑏 ∈ V ∃ 𝑘 ∈ Poset 𝑏 = ( ( Base ↾ Poset ) ‘ 𝑘 )
13		dffo3	⊢ ( ( Base ↾ Poset ) : Poset –onto→ V ↔ ( ( Base ↾ Poset ) : Poset ⟶ V ∧ ∀ 𝑏 ∈ V ∃ 𝑘 ∈ Poset 𝑏 = ( ( Base ↾ Poset ) ‘ 𝑘 ) ) )
14	6 12 13	mpbir2an	⊢ ( Base ↾ Poset ) : Poset –onto→ V