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

Metamath Proof Explorer

Theorem 00ply1bas

Description: Lemma for ply1basfvi and deg1fvi . (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Assertion 00ply1bas ∅ = ( Base ‘ ( Poly1 ‘ ∅ ) )

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ 𝑎 ∈ ∅
2 noel ⊢ ¬ ( 𝑎 ‘ ( 1o × { 0 } ) ) ∈ ∅
3 eqid ⊢ ( Poly1 ‘ ∅ ) = ( Poly1 ‘ ∅ )
4 eqid ⊢ ( Base ‘ ( Poly1 ‘ ∅ ) ) = ( Base ‘ ( Poly1 ‘ ∅ ) )
5 base0 ⊢ ∅ = ( Base ‘ ∅ )
6 3 4 5 ply1basf ⊢ ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ∅ ) ) → 𝑎 : ( ℕ0 ↑m 1o ) ⟶ ∅ )
7 0nn0 ⊢ 0 ∈ ℕ0
8 7 fconst6 ⊢ ( 1o × { 0 } ) : 1o ⟶ ℕ0
9 nn0ex ⊢ ℕ0 ∈ V
10 1oex ⊢ 1o ∈ V
11 9 10 elmap ⊢ ( ( 1o × { 0 } ) ∈ ( ℕ0 ↑m 1o ) ↔ ( 1o × { 0 } ) : 1o ⟶ ℕ0 )
12 8 11 mpbir ⊢ ( 1o × { 0 } ) ∈ ( ℕ0 ↑m 1o )
13 ffvelcdm ⊢ ( ( 𝑎 : ( ℕ0 ↑m 1o ) ⟶ ∅ ∧ ( 1o × { 0 } ) ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑎 ‘ ( 1o × { 0 } ) ) ∈ ∅ )
14 6 12 13 sylancl ⊢ ( 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ∅ ) ) → ( 𝑎 ‘ ( 1o × { 0 } ) ) ∈ ∅ )
15 2 14 mto ⊢ ¬ 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ∅ ) )
16 1 15 2false ⊢ ( 𝑎 ∈ ∅ ↔ 𝑎 ∈ ( Base ‘ ( Poly1 ‘ ∅ ) ) )
17 16 eqriv ⊢ ∅ = ( Base ‘ ( Poly1 ‘ ∅ ) )