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 e. RR
	axlowdimlem4.2	|- B e. RR
Assertion	axlowdimlem4	|- { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> RR

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem4.1	|- A e. RR
2		axlowdimlem4.2	|- B e. RR
3		1ne2	|- 1 =/= 2
4		1ex	|- 1 e. _V
5		2ex	|- 2 e. _V
6	1	elexi	|- A e. _V
7	2	elexi	|- B e. _V
8	4 5 6 7	fpr	|- ( 1 =/= 2 -> { <. 1 , A >. , <. 2 , B >. } : { 1 , 2 } --> { A , B } )
9	3 8	ax-mp	|- { <. 1 , A >. , <. 2 , B >. } : { 1 , 2 } --> { A , B }
10		fz12pr	|- ( 1 ... 2 ) = { 1 , 2 }
11	10	feq2i	|- ( { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> { A , B } <-> { <. 1 , A >. , <. 2 , B >. } : { 1 , 2 } --> { A , B } )
12	9 11	mpbir	|- { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> { A , B }
13	1 2	pm3.2i	|- ( A e. RR /\ B e. RR )
14	6 7	prss	|- ( ( A e. RR /\ B e. RR ) <-> { A , B } C_ RR )
15	13 14	mpbi	|- { A , B } C_ RR
16		fss	|- ( ( { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> { A , B } /\ { A , B } C_ RR ) -> { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> RR )
17	12 15 16	mp2an	|- { <. 1 , A >. , <. 2 , B >. } : ( 1 ... 2 ) --> RR