Metamath Proof Explorer


Theorem leiso

Description: Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion leiso A*B*FIsom<,<ABFIsom,AB

Proof

Step Hyp Ref Expression
1 df-le =*×*<-1
2 1 ineq1i A×A=*×*<-1A×A
3 indif1 *×*<-1A×A=*×*A×A<-1
4 2 3 eqtri A×A=*×*A×A<-1
5 xpss12 A*A*A×A*×*
6 5 anidms A*A×A*×*
7 sseqin2 A×A*×**×*A×A=A×A
8 6 7 sylib A**×*A×A=A×A
9 8 difeq1d A**×*A×A<-1=A×A<-1
10 4 9 eqtr2id A*A×A<-1=A×A
11 isoeq2 A×A<-1=A×AFIsomA×A<-1,B×B<-1ABFIsomA×A,B×B<-1AB
12 10 11 syl A*FIsomA×A<-1,B×B<-1ABFIsomA×A,B×B<-1AB
13 1 ineq1i B×B=*×*<-1B×B
14 indif1 *×*<-1B×B=*×*B×B<-1
15 13 14 eqtri B×B=*×*B×B<-1
16 xpss12 B*B*B×B*×*
17 16 anidms B*B×B*×*
18 sseqin2 B×B*×**×*B×B=B×B
19 17 18 sylib B**×*B×B=B×B
20 19 difeq1d B**×*B×B<-1=B×B<-1
21 15 20 eqtr2id B*B×B<-1=B×B
22 isoeq3 B×B<-1=B×BFIsomA×A,B×B<-1ABFIsomA×A,B×BAB
23 21 22 syl B*FIsomA×A,B×B<-1ABFIsomA×A,B×BAB
24 12 23 sylan9bb A*B*FIsomA×A<-1,B×B<-1ABFIsomA×A,B×BAB
25 isocnv2 FIsom<,<ABFIsom<-1,<-1AB
26 eqid A×A<-1=A×A<-1
27 eqid B×B<-1=B×B<-1
28 26 27 isocnv3 FIsom<-1,<-1ABFIsomA×A<-1,B×B<-1AB
29 25 28 bitri FIsom<,<ABFIsomA×A<-1,B×B<-1AB
30 isores1 FIsom,ABFIsomA×A,AB
31 isores2 FIsomA×A,ABFIsomA×A,B×BAB
32 30 31 bitri FIsom,ABFIsomA×A,B×BAB
33 24 29 32 3bitr4g A*B*FIsom<,<ABFIsom,AB