Theorem axlowdimlem4

Description: Lemma for axlowdim . Set up a particular constant function. (Contributed by Scott Fenton, 17-Apr-2013)

	Ref	Expression
Hypotheses	axlowdimlem4.1	$$⊢A\in ℝ$$
	axlowdimlem4.2	$$⊢B\in ℝ$$
Assertion	axlowdimlem4	$$⊢\left\{⟨1,A⟩,⟨2,B⟩\right\}:\left(1\dots 2\right)⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem4.1	$$⊢A\in ℝ$$
2		axlowdimlem4.2	$$⊢B\in ℝ$$
3		1ne2	$$⊢1\ne 2$$
4		1ex	$$⊢1\in \mathrm{V}$$
5		2ex	$$⊢2\in \mathrm{V}$$
6	1	elexi	$$⊢A\in \mathrm{V}$$
7	2	elexi	$$⊢B\in \mathrm{V}$$
8	4 5 6 7	fpr	$$⊢1\ne 2\to \left\{⟨1,A⟩,⟨2,B⟩\right\}:\left\{1,2\right\}⟶\left\{A,B\right\}$$
9	3 8	ax-mp	$$⊢\left\{⟨1,A⟩,⟨2,B⟩\right\}:\left\{1,2\right\}⟶\left\{A,B\right\}$$
10		fz12pr	$$⊢\left(1\dots 2\right)=\left\{1,2\right\}$$
11	10	feq2i	$$⊢\left\{⟨1,A⟩,⟨2,B⟩\right\}:\left(1\dots 2\right)⟶\left\{A,B\right\}\leftrightarrow \left\{⟨1,A⟩,⟨2,B⟩\right\}:\left\{1,2\right\}⟶\left\{A,B\right\}$$
12	9 11	mpbir	$$⊢\left\{⟨1,A⟩,⟨2,B⟩\right\}:\left(1\dots 2\right)⟶\left\{A,B\right\}$$
13	1 2	pm3.2i	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)$$
14	6 7	prss	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\leftrightarrow \left\{A,B\right\}\subseteq ℝ$$
15	13 14	mpbi	$$⊢\left\{A,B\right\}\subseteq ℝ$$
16		fss	$$⊢\left(\left\{⟨1,A⟩,⟨2,B⟩\right\}:\left(1\dots 2\right)⟶\left\{A,B\right\}\wedge \left\{A,B\right\}\subseteq ℝ\right)\to \left\{⟨1,A⟩,⟨2,B⟩\right\}:\left(1\dots 2\right)⟶ℝ$$
17	12 15 16	mp2an	$$⊢\left\{⟨1,A⟩,⟨2,B⟩\right\}:\left(1\dots 2\right)⟶ℝ$$