00ply1bas

		Ref	Expression
	Assertion	00ply1bas	$⊢ \emptyset = {Base}_{{Poly}_{1} (\emptyset)}$

Step	Hyp	Ref	Expression
1		noel	$⊢ \neg a \in \emptyset$
2		noel	$⊢ \neg a (1_{𝑜} \times \{0\}) \in \emptyset$
3		eqid	$⊢ {Poly}_{1} (\emptyset) = {Poly}_{1} (\emptyset)$
4		eqid	$⊢ {Base}_{{Poly}_{1} (\emptyset)} = {Base}_{{Poly}_{1} (\emptyset)}$
5		base0	$⊢ \emptyset = {Base}_{\emptyset}$
6	3 4 5	ply1basf	$⊢ a \in {Base}_{{Poly}_{1} (\emptyset)} \to a : {ℕ_{0}}^{1_{𝑜}} ⟶ \emptyset$
7		0nn0	$⊢ 0 \in ℕ_{0}$
8	7	fconst6	$⊢ (1_{𝑜} \times \{0\}) : 1_{𝑜} ⟶ ℕ_{0}$
9		nn0ex	$⊢ ℕ_{0} \in V$
10		1oex	$⊢ 1_{𝑜} \in V$
11	9 10	elmap	$⊢ 1_{𝑜} \times \{0\} \in ({ℕ_{0}}^{1_{𝑜}}) \leftrightarrow (1_{𝑜} \times \{0\}) : 1_{𝑜} ⟶ ℕ_{0}$
12	8 11	mpbir	$⊢ 1_{𝑜} \times \{0\} \in ({ℕ_{0}}^{1_{𝑜}})$
13		ffvelcdm	$⊢ (a : {ℕ_{0}}^{1_{𝑜}} ⟶ \emptyset \land 1_{𝑜} \times \{0\} \in ({ℕ_{0}}^{1_{𝑜}})) \to a (1_{𝑜} \times \{0\}) \in \emptyset$
14	6 12 13	sylancl	$⊢ a \in {Base}_{{Poly}_{1} (\emptyset)} \to a (1_{𝑜} \times \{0\}) \in \emptyset$
15	2 14	mto	$⊢ \neg a \in {Base}_{{Poly}_{1} (\emptyset)}$
16	1 15	2false	$⊢ a \in \emptyset \leftrightarrow a \in {Base}_{{Poly}_{1} (\emptyset)}$
17	16	eqriv	$⊢ \emptyset = {Base}_{{Poly}_{1} (\emptyset)}$

Metamath Proof Explorer