Theorem coe1mul2lem1

Description: An equivalence for coe1mul2 . (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Assertion	coe1mul2lem1	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(X{\le }_f\left(1_{𝑜}\times \left\{A\right\}\right)\leftrightarrow X\left(\varnothing \right)\in \left(0\dots A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
2	1	a1i	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to 1_{𝑜}\in \mathrm{On}$$
3		fvexd	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\wedge a\in 1_{𝑜}\right)\to X\left(\varnothing \right)\in \mathrm{V}$$
4		simpll	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\wedge a\in 1_{𝑜}\right)\to A\in {\mathbb{N}}_0$$
5		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
6		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
7		0ex	$$⊢\varnothing \in \mathrm{V}$$
8	5 6 7	mapsnconst	$$⊢X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to X=1_{𝑜}\times \left\{X\left(\varnothing \right)\right\}$$
9	8	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to X=1_{𝑜}\times \left\{X\left(\varnothing \right)\right\}$$
10		fconstmpt	$$⊢1_{𝑜}\times \left\{X\left(\varnothing \right)\right\}=\left(a\in 1_{𝑜}⟼X\left(\varnothing \right)\right)$$
11	9 10	eqtrdi	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to X=\left(a\in 1_{𝑜}⟼X\left(\varnothing \right)\right)$$
12		fconstmpt	$$⊢1_{𝑜}\times \left\{A\right\}=\left(a\in 1_{𝑜}⟼A\right)$$
13	12	a1i	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to 1_{𝑜}\times \left\{A\right\}=\left(a\in 1_{𝑜}⟼A\right)$$
14	2 3 4 11 13	ofrfval2	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(X{\le }_f\left(1_{𝑜}\times \left\{A\right\}\right)\leftrightarrow \forall a\in 1_{𝑜}X\left(\varnothing \right)\le A\right)$$
15		1n0	$$⊢1_{𝑜}\ne \varnothing$$
16		r19.3rzv	$$⊢1_{𝑜}\ne \varnothing \to \left(X\left(\varnothing \right)\le A\leftrightarrow \forall a\in 1_{𝑜}X\left(\varnothing \right)\le A\right)$$
17	15 16	mp1i	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(X\left(\varnothing \right)\le A\leftrightarrow \forall a\in 1_{𝑜}X\left(\varnothing \right)\le A\right)$$
18		elmapi	$$⊢X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to X:1_{𝑜}⟶{\mathbb{N}}_0$$
19		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
20		ffvelcdm	$$⊢\left(X:1_{𝑜}⟶{\mathbb{N}}_0\wedge \varnothing \in 1_{𝑜}\right)\to X\left(\varnothing \right)\in {\mathbb{N}}_0$$
21	18 19 20	sylancl	$$⊢X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to X\left(\varnothing \right)\in {\mathbb{N}}_0$$
22	21	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to X\left(\varnothing \right)\in {\mathbb{N}}_0$$
23	22	biantrurd	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(X\left(\varnothing \right)\le A\leftrightarrow \left(X\left(\varnothing \right)\in {\mathbb{N}}_0\wedge X\left(\varnothing \right)\le A\right)\right)$$
24		fznn0	$$⊢A\in {\mathbb{N}}_0\to \left(X\left(\varnothing \right)\in \left(0\dots A\right)\leftrightarrow \left(X\left(\varnothing \right)\in {\mathbb{N}}_0\wedge X\left(\varnothing \right)\le A\right)\right)$$
25	24	adantr	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(X\left(\varnothing \right)\in \left(0\dots A\right)\leftrightarrow \left(X\left(\varnothing \right)\in {\mathbb{N}}_0\wedge X\left(\varnothing \right)\le A\right)\right)$$
26	23 25	bitr4d	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(X\left(\varnothing \right)\le A\leftrightarrow X\left(\varnothing \right)\in \left(0\dots A\right)\right)$$
27	14 17 26	3bitr2d	$$⊢\left(A\in {\mathbb{N}}_0\wedge X\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(X{\le }_f\left(1_{𝑜}\times \left\{A\right\}\right)\leftrightarrow X\left(\varnothing \right)\in \left(0\dots A\right)\right)$$