Metamath Proof Explorer

Theorem gtiso

Description: Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017)

Ref Expression
Assertion gtiso ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom < , ◡ < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ( 𝐴 × 𝐴 ) ∖ < ) = ( ( 𝐴 × 𝐴 ) ∖ < )
2 eqid ⊢ ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) = ( ( 𝐵 × 𝐵 ) ∖ ◡ < )
3 1 2 isocnv3 ⊢ ( 𝐹 Isom < , ◡ < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) )
4 3 a1i ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom < , ◡ < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ) )
5 df-le ⊢ ≤ = ( ( ℝ* × ℝ* ) ∖ ◡ < )
6 5 cnveqi ⊢ ◡ ≤ = ◡ ( ( ℝ* × ℝ* ) ∖ ◡ < )
7 cnvdif ⊢ ◡ ( ( ℝ* × ℝ* ) ∖ ◡ < ) = ( ◡ ( ℝ* × ℝ* ) ∖ ◡ ◡ < )
8 cnvxp ⊢ ◡ ( ℝ* × ℝ* ) = ( ℝ* × ℝ* )
9 ltrel ⊢ Rel <
10 dfrel2 ⊢ ( Rel < ↔ ◡ ◡ < = < )
11 9 10 mpbi ⊢ ◡ ◡ < = <
12 8 11 difeq12i ⊢ ( ◡ ( ℝ* × ℝ* ) ∖ ◡ ◡ < ) = ( ( ℝ* × ℝ* ) ∖ < )
13 6 7 12 3eqtri ⊢ ◡ ≤ = ( ( ℝ* × ℝ* ) ∖ < )
14 13 ineq1i ⊢ ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( ℝ* × ℝ* ) ∖ < ) ∩ ( 𝐴 × 𝐴 ) )
15 indif1 ⊢ ( ( ( ℝ* × ℝ* ) ∖ < ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) ∖ < )
16 14 15 eqtri ⊢ ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) ∖ < )
17 xpss12 ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐴 ⊆ ℝ* ) → ( 𝐴 × 𝐴 ) ⊆ ( ℝ* × ℝ* ) )
18 17 anidms ⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 × 𝐴 ) ⊆ ( ℝ* × ℝ* ) )
19 sseqin2 ⊢ ( ( 𝐴 × 𝐴 ) ⊆ ( ℝ* × ℝ* ) ↔ ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
20 18 19 sylib ⊢ ( 𝐴 ⊆ ℝ* → ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
21 20 difeq1d ⊢ ( 𝐴 ⊆ ℝ* → ( ( ( ℝ* × ℝ* ) ∩ ( 𝐴 × 𝐴 ) ) ∖ < ) = ( ( 𝐴 × 𝐴 ) ∖ < ) )
22 16 21 syl5req ⊢ ( 𝐴 ⊆ ℝ* → ( ( 𝐴 × 𝐴 ) ∖ < ) = ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) )
23 22 adantr ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( ( 𝐴 × 𝐴 ) ∖ < ) = ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) )
24 isoeq2 ⊢ ( ( ( 𝐴 × 𝐴 ) ∖ < ) = ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) → ( 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ) )
25 23 24 syl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom ( ( 𝐴 × 𝐴 ) ∖ < ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ) )
26 5 ineq1i ⊢ ( ≤ ∩ ( 𝐵 × 𝐵 ) ) = ( ( ( ℝ* × ℝ* ) ∖ ◡ < ) ∩ ( 𝐵 × 𝐵 ) )
27 indif1 ⊢ ( ( ( ℝ* × ℝ* ) ∖ ◡ < ) ∩ ( 𝐵 × 𝐵 ) ) = ( ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) ∖ ◡ < )
28 26 27 eqtri ⊢ ( ≤ ∩ ( 𝐵 × 𝐵 ) ) = ( ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) ∖ ◡ < )
29 xpss12 ⊢ ( ( 𝐵 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐵 × 𝐵 ) ⊆ ( ℝ* × ℝ* ) )
30 29 anidms ⊢ ( 𝐵 ⊆ ℝ* → ( 𝐵 × 𝐵 ) ⊆ ( ℝ* × ℝ* ) )
31 sseqin2 ⊢ ( ( 𝐵 × 𝐵 ) ⊆ ( ℝ* × ℝ* ) ↔ ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) = ( 𝐵 × 𝐵 ) )
32 30 31 sylib ⊢ ( 𝐵 ⊆ ℝ* → ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) = ( 𝐵 × 𝐵 ) )
33 32 difeq1d ⊢ ( 𝐵 ⊆ ℝ* → ( ( ( ℝ* × ℝ* ) ∩ ( 𝐵 × 𝐵 ) ) ∖ ◡ < ) = ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) )
34 28 33 syl5req ⊢ ( 𝐵 ⊆ ℝ* → ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) = ( ≤ ∩ ( 𝐵 × 𝐵 ) ) )
35 34 adantl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) = ( ≤ ∩ ( 𝐵 × 𝐵 ) ) )
36 isoeq3 ⊢ ( ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) = ( ≤ ∩ ( 𝐵 × 𝐵 ) ) → ( 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) ) )
37 35 36 syl ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ( 𝐵 × 𝐵 ) ∖ ◡ < ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) ) )
38 4 25 37 3bitrd ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom < , ◡ < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) ) )
39 isocnv2 ⊢ ( 𝐹 Isom ◡ ≤ , ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ◡ ◡ ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) )
40 isores2 ⊢ ( 𝐹 Isom ◡ ≤ , ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ◡ ≤ , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) )
41 isores1 ⊢ ( 𝐹 Isom ◡ ≤ , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) )
42 40 41 bitri ⊢ ( 𝐹 Isom ◡ ≤ , ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) )
43 lerel ⊢ Rel ≤
44 dfrel2 ⊢ ( Rel ≤ ↔ ◡ ◡ ≤ = ≤ )
45 43 44 mpbi ⊢ ◡ ◡ ≤ = ≤
46 isoeq2 ⊢ ( ◡ ◡ ≤ = ≤ → ( 𝐹 Isom ◡ ◡ ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) ) )
47 45 46 ax-mp ⊢ ( 𝐹 Isom ◡ ◡ ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) )
48 39 42 47 3bitr3ri ⊢ ( 𝐹 Isom ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ( ◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) , ( ≤ ∩ ( 𝐵 × 𝐵 ) ) ( 𝐴 , 𝐵 ) )
49 38 48 bitr4di ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ* ) → ( 𝐹 Isom < , ◡ < ( 𝐴 , 𝐵 ) ↔ 𝐹 Isom ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) ) )