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 ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ≤ , ≤ ( 𝐴 , 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 df-le ⊢ ≤ = ( ( ℝ* × ℝ* ) ∖ ◡ < )
2 1 ineq1i ⊢ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( ℝ* × ℝ* ) ∖ ◡ < ) ∩ ( 𝐴 × 𝐴 ) )
3 indif1 ⊢ ( ( ( ℝ* × ℝ* ) ∖ ◡ < ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) ∖ ◡ < )
4 2 3 eqtri ⊢ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) ∖ ◡ < )
5 xpss12 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ⊆ ℝ* ) → ( 𝐴 × 𝐴 ) ⊆ ( ℝ* × ℝ* ) )
6 5 anidms ⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 × 𝐴 ) ⊆ ( ℝ* × ℝ* ) )
7 sseqin2 ⊢ ( ( 𝐴 × 𝐴 ) ⊆ ( ℝ* × ℝ* ) ↔ ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
8 6 7 sylib ⊢ ( 𝐴 ⊆ ℝ* → ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
9 8 difeq1d ⊢ ( 𝐴 ⊆ ℝ* → ( ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) ∖ ◡ < ) = ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) )
10 4 9 syl5req ⊢ ( 𝐴 ⊆ ℝ* → ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) = ( ≤ ∩ ( 𝐴 × 𝐴 ) ) )
11 isoeq2 ⊢ ( ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) = ( ≤ ∩ ( 𝐴 × 𝐴 ) ) → ( 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ) )
12 10 11 syl ⊢ ( 𝐴 ⊆ ℝ* → ( 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ) )
13 1 ineq1i ⊢ ( ≤ ∩ ( 𝐵 × 𝐵 ) ) = ( ( ( ℝ* × ℝ* ) ∖ ◡ < ) ∩ ( 𝐵 × 𝐵 ) )
14 indif1 ⊢ ( ( ( ℝ* × ℝ* ) ∖ ◡ < ) ∩ ( 𝐵 × 𝐵 ) ) = ( ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) ∖ ◡ < )
15 13 14 eqtri ⊢ ( ≤ ∩ ( 𝐵 × 𝐵 ) ) = ( ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) ∖ ◡ < )
16 xpss12 ⊢ ( ( 𝐵 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐵 × 𝐵 ) ⊆ ( ℝ* × ℝ* ) )
17 16 anidms ⊢ ( 𝐵 ⊆ ℝ* → ( 𝐵 × 𝐵 ) ⊆ ( ℝ* × ℝ* ) )
18 sseqin2 ⊢ ( ( 𝐵 × 𝐵 ) ⊆ ( ℝ* × ℝ* ) ↔ ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) = ( 𝐵 × 𝐵 ) )
19 17 18 sylib ⊢ ( 𝐵 ⊆ ℝ* → ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) = ( 𝐵 × 𝐵 ) )
20 19 difeq1d ⊢ ( 𝐵 ⊆ ℝ* → ( ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) ∖ ◡ < ) = ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) )
21 15 20 syl5req ⊢ ( 𝐵 ⊆ ℝ* → ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) = ( ≤ ∩ ( 𝐵 × 𝐵 ) ) )
22 isoeq3 ⊢ ( ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) = ( ≤ ∩ ( 𝐵 × 𝐵 ) ) → ( 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) ) )
23 21 22 syl ⊢ ( 𝐵 ⊆ ℝ* → ( 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) ) )
24 12 23 sylan9bb ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) ) )
25 isocnv2 ⊢ ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ◡ < , ◡ < ( 𝐴 , 𝐵 ) )
26 eqid ⊢ ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) = ( ( 𝐴 × 𝐴 ) ∖ ◡ < )
27 eqid ⊢ ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) = ( ( 𝐵 × 𝐵 ) ∖ ◡ < )
28 26 27 isocnv3 ⊢ ( 𝐹 Isom ◡ < , ◡ < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) )
29 25 28 bitri ⊢ ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ ◡ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) )
30 isores1 ⊢ ( 𝐹 Isom ≤ , ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ≤ ( 𝐴 , 𝐵 ) )
31 isores2 ⊢ ( 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) )
32 30 31 bitri ⊢ ( 𝐹 Isom ≤ , ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) )
33 24 29 32 3bitr4g ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom < , < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ≤ , ≤ ( 𝐴 , 𝐵 ) ) )