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

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 ⊢ ( 𝑏 ∈ 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