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		ffvelrn	⊢ ( ( 𝑎 : ( ℕ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 ‘ ∅ ) )