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 * F Isom < , < A B F Isom , A B

Proof

Step Hyp Ref Expression
1 df-le = * × * < -1
2 1 ineq1i A × A = * × * < -1 A × A
3 indif1 * × * < -1 A × 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 × A F Isom A × A < -1 , B × B < -1 A B F Isom A × A , B × B < -1 A B
12 10 11 syl A * F Isom A × A < -1 , B × B < -1 A B F Isom A × A , B × B < -1 A B
13 1 ineq1i B × B = * × * < -1 B × B
14 indif1 * × * < -1 B × 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 × B F Isom A × A , B × B < -1 A B F Isom A × A , B × B A B
23 21 22 syl B * F Isom A × A , B × B < -1 A B F Isom A × A , B × B A B
24 12 23 sylan9bb A * B * F Isom A × A < -1 , B × B < -1 A B F Isom A × A , B × B A B
25 isocnv2 F Isom < , < A B F Isom < -1 , < -1 A B
26 eqid A × A < -1 = A × A < -1
27 eqid B × B < -1 = B × B < -1
28 26 27 isocnv3 F Isom < -1 , < -1 A B F Isom A × A < -1 , B × B < -1 A B
29 25 28 bitri F Isom < , < A B F Isom A × A < -1 , B × B < -1 A B
30 isores1 F Isom , A B F Isom A × A , A B
31 isores2 F Isom A × A , A B F Isom A × A , B × B A B
32 30 31 bitri F Isom , A B F Isom A × A , B × B A B
33 24 29 32 3bitr4g A * B * F Isom < , < A B F Isom , A B