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 |