Metamath Proof Explorer

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 ⊢ b ∈ V → ∃ k ∈ Poset b = Base k
8 fvres ⊢ k ∈ Poset → Base ↾ Poset ⁡ k = Base k
9 8 eqeq2d ⊢ k ∈ Poset → b = Base ↾ Poset ⁡ k ↔ b = Base k
10 9 rexbiia ⊢ ∃ k ∈ Poset b = Base ↾ Poset ⁡ k ↔ ∃ k ∈ Poset b = Base k
11 7 10 sylibr ⊢ b ∈ V → ∃ k ∈ Poset b = Base ↾ Poset ⁡ k
12 11 rgen ⊢ ∀ b ∈ V ∃ k ∈ Poset b = Base ↾ Poset ⁡ k
13 dffo3 ⊢ Base ↾ Poset : Poset ⟶ onto V ↔ Base ↾ Poset : Poset ⟶ V ∧ ∀ b ∈ V ∃ k ∈ Poset b = Base ↾ Poset ⁡ k
14 6 12 13 mpbir2an ⊢ Base ↾ Poset : Poset ⟶ onto V