Proof of Theorem gtiso
Step | Hyp | Ref
| Expression |
1 | | eqid 2824 |
. . . . 5
⊢ ((𝐴 × 𝐴) ∖ < ) = ((𝐴 × 𝐴) ∖ < ) |
2 | | eqid 2824 |
. . . . 5
⊢ ((𝐵 × 𝐵) ∖ ◡ < ) = ((𝐵 × 𝐵) ∖ ◡ < ) |
3 | 1, 2 | isocnv3 7088 |
. . . 4
⊢ (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵)) |
4 | 3 | a1i 11 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
5 | | df-le 10684 |
. . . . . . . . . 10
⊢ ≤ =
((ℝ* × ℝ*) ∖ ◡ < ) |
6 | 5 | cnveqi 5748 |
. . . . . . . . 9
⊢ ◡ ≤ = ◡((ℝ* ×
ℝ*) ∖ ◡ <
) |
7 | | cnvdif 6005 |
. . . . . . . . 9
⊢ ◡((ℝ* ×
ℝ*) ∖ ◡ < ) =
(◡(ℝ* ×
ℝ*) ∖ ◡◡ < ) |
8 | | cnvxp 6017 |
. . . . . . . . . 10
⊢ ◡(ℝ* ×
ℝ*) = (ℝ* ×
ℝ*) |
9 | | ltrel 10706 |
. . . . . . . . . . 11
⊢ Rel
< |
10 | | dfrel2 6049 |
. . . . . . . . . . 11
⊢ (Rel <
↔ ◡◡ < = < ) |
11 | 9, 10 | mpbi 232 |
. . . . . . . . . 10
⊢ ◡◡
< = < |
12 | 8, 11 | difeq12i 4100 |
. . . . . . . . 9
⊢ (◡(ℝ* ×
ℝ*) ∖ ◡◡ < ) = ((ℝ* ×
ℝ*) ∖ < ) |
13 | 6, 7, 12 | 3eqtri 2851 |
. . . . . . . 8
⊢ ◡ ≤ = ((ℝ* ×
ℝ*) ∖ < ) |
14 | 13 | ineq1i 4188 |
. . . . . . 7
⊢ (◡ ≤ ∩ (𝐴 × 𝐴)) = (((ℝ* ×
ℝ*) ∖ < ) ∩ (𝐴 × 𝐴)) |
15 | | indif1 4251 |
. . . . . . 7
⊢
(((ℝ* × ℝ*) ∖ < ) ∩
(𝐴 × 𝐴)) = (((ℝ*
× ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) |
16 | 14, 15 | eqtri 2847 |
. . . . . 6
⊢ (◡ ≤ ∩ (𝐴 × 𝐴)) = (((ℝ* ×
ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) |
17 | | xpss12 5573 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐴 ⊆
ℝ*) → (𝐴 × 𝐴) ⊆ (ℝ* ×
ℝ*)) |
18 | 17 | anidms 569 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ (𝐴 × 𝐴) ⊆ (ℝ*
× ℝ*)) |
19 | | sseqin2 4195 |
. . . . . . . 8
⊢ ((𝐴 × 𝐴) ⊆ (ℝ* ×
ℝ*) ↔ ((ℝ* × ℝ*)
∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) |
20 | 18, 19 | sylib 220 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ*
→ ((ℝ* × ℝ*) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) |
21 | 20 | difeq1d 4101 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ*
→ (((ℝ* × ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) = ((𝐴 × 𝐴) ∖ < )) |
22 | 16, 21 | syl5req 2872 |
. . . . 5
⊢ (𝐴 ⊆ ℝ*
→ ((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴))) |
23 | 22 | adantr 483 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → ((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴))) |
24 | | isoeq2 7074 |
. . . 4
⊢ (((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴)) → (𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
25 | 23, 24 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
26 | 5 | ineq1i 4188 |
. . . . . . 7
⊢ ( ≤
∩ (𝐵 × 𝐵)) = (((ℝ*
× ℝ*) ∖ ◡
< ) ∩ (𝐵 ×
𝐵)) |
27 | | indif1 4251 |
. . . . . . 7
⊢
(((ℝ* × ℝ*) ∖ ◡ < ) ∩ (𝐵 × 𝐵)) = (((ℝ* ×
ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) |
28 | 26, 27 | eqtri 2847 |
. . . . . 6
⊢ ( ≤
∩ (𝐵 × 𝐵)) = (((ℝ*
× ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) |
29 | | xpss12 5573 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐵 × 𝐵) ⊆ (ℝ* ×
ℝ*)) |
30 | 29 | anidms 569 |
. . . . . . . 8
⊢ (𝐵 ⊆ ℝ*
→ (𝐵 × 𝐵) ⊆ (ℝ*
× ℝ*)) |
31 | | sseqin2 4195 |
. . . . . . . 8
⊢ ((𝐵 × 𝐵) ⊆ (ℝ* ×
ℝ*) ↔ ((ℝ* × ℝ*)
∩ (𝐵 × 𝐵)) = (𝐵 × 𝐵)) |
32 | 30, 31 | sylib 220 |
. . . . . . 7
⊢ (𝐵 ⊆ ℝ*
→ ((ℝ* × ℝ*) ∩ (𝐵 × 𝐵)) = (𝐵 × 𝐵)) |
33 | 32 | difeq1d 4101 |
. . . . . 6
⊢ (𝐵 ⊆ ℝ*
→ (((ℝ* × ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) = ((𝐵 × 𝐵) ∖ ◡ < )) |
34 | 28, 33 | syl5req 2872 |
. . . . 5
⊢ (𝐵 ⊆ ℝ*
→ ((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵))) |
35 | 34 | adantl 484 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → ((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵))) |
36 | | isoeq3 7075 |
. . . 4
⊢ (((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵)) → (𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
37 | 35, 36 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
38 | 4, 25, 37 | 3bitrd 307 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
39 | | isocnv2 7087 |
. . 3
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ◡◡
≤ , ◡ ≤ (𝐴, 𝐵)) |
40 | | isores2 7089 |
. . . 4
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ◡ ≤ , ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
41 | | isores1 7090 |
. . . 4
⊢ (𝐹 Isom ◡ ≤ , ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
42 | 40, 41 | bitri 277 |
. . 3
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
43 | | lerel 10708 |
. . . . 5
⊢ Rel
≤ |
44 | | dfrel2 6049 |
. . . . 5
⊢ (Rel ≤
↔ ◡◡ ≤ = ≤ ) |
45 | 43, 44 | mpbi 232 |
. . . 4
⊢ ◡◡
≤ = ≤ |
46 | | isoeq2 7074 |
. . . 4
⊢ (◡◡
≤ = ≤ → (𝐹 Isom
◡◡ ≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) |
47 | 45, 46 | ax-mp 5 |
. . 3
⊢ (𝐹 Isom ◡◡
≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵)) |
48 | 39, 42, 47 | 3bitr3ri 304 |
. 2
⊢ (𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
49 | 38, 48 | syl6bbr 291 |
1
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) |