Metamath Proof Explorer


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