Theorem axlowdimlem4

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

	Ref	Expression
Hypotheses	axlowdimlem4.1	⊢ 𝐴 ∈ ℝ
	axlowdimlem4.2	⊢ 𝐵 ∈ ℝ
Assertion	axlowdimlem4	⊢ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ ℝ

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem4.1	⊢ 𝐴 ∈ ℝ
2		axlowdimlem4.2	⊢ 𝐵 ∈ ℝ
3		1ne2	⊢ 1 ≠ 2
4		1ex	⊢ 1 ∈ V
5		2ex	⊢ 2 ∈ V
6	1	elexi	⊢ 𝐴 ∈ V
7	2	elexi	⊢ 𝐵 ∈ V
8	4 5 6 7	fpr	⊢ ( 1 ≠ 2 → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : { 1 , 2 } ⟶ { 𝐴 , 𝐵 } )
9	3 8	ax-mp	⊢ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : { 1 , 2 } ⟶ { 𝐴 , 𝐵 }
10		fz12pr	⊢ ( 1 ... 2 ) = { 1 , 2 }
11	10	feq2i	⊢ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ { 𝐴 , 𝐵 } ↔ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : { 1 , 2 } ⟶ { 𝐴 , 𝐵 } )
12	9 11	mpbir	⊢ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ { 𝐴 , 𝐵 }
13	1 2	pm3.2i	⊢ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ )
14	6 7	prss	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ↔ { 𝐴 , 𝐵 } ⊆ ℝ )
15	13 14	mpbi	⊢ { 𝐴 , 𝐵 } ⊆ ℝ
16		fss	⊢ ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } ⊆ ℝ ) → { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ ℝ )
17	12 15 16	mp2an	⊢ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ ℝ