Proof of Theorem gtiso
Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
⊢ ((𝐴 × 𝐴) ∖ < ) = ((𝐴 × 𝐴) ∖ < ) |
2 | | eqid 2737 |
. . . . 5
⊢ ((𝐵 × 𝐵) ∖ ◡ < ) = ((𝐵 × 𝐵) ∖ ◡ < ) |
3 | 1, 2 | isocnv3 7141 |
. . . 4
⊢ (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵)) |
4 | 3 | a1i 11 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
5 | | df-le 10873 |
. . . . . . . . . 10
⊢ ≤ =
((ℝ* × ℝ*) ∖ ◡ < ) |
6 | 5 | cnveqi 5743 |
. . . . . . . . 9
⊢ ◡ ≤ = ◡((ℝ* ×
ℝ*) ∖ ◡ <
) |
7 | | cnvdif 6007 |
. . . . . . . . 9
⊢ ◡((ℝ* ×
ℝ*) ∖ ◡ < ) =
(◡(ℝ* ×
ℝ*) ∖ ◡◡ < ) |
8 | | cnvxp 6020 |
. . . . . . . . . 10
⊢ ◡(ℝ* ×
ℝ*) = (ℝ* ×
ℝ*) |
9 | | ltrel 10895 |
. . . . . . . . . . 11
⊢ Rel
< |
10 | | dfrel2 6052 |
. . . . . . . . . . 11
⊢ (Rel <
↔ ◡◡ < = < ) |
11 | 9, 10 | mpbi 233 |
. . . . . . . . . 10
⊢ ◡◡
< = < |
12 | 8, 11 | difeq12i 4035 |
. . . . . . . . 9
⊢ (◡(ℝ* ×
ℝ*) ∖ ◡◡ < ) = ((ℝ* ×
ℝ*) ∖ < ) |
13 | 6, 7, 12 | 3eqtri 2769 |
. . . . . . . 8
⊢ ◡ ≤ = ((ℝ* ×
ℝ*) ∖ < ) |
14 | 13 | ineq1i 4123 |
. . . . . . 7
⊢ (◡ ≤ ∩ (𝐴 × 𝐴)) = (((ℝ* ×
ℝ*) ∖ < ) ∩ (𝐴 × 𝐴)) |
15 | | indif1 4186 |
. . . . . . 7
⊢
(((ℝ* × ℝ*) ∖ < ) ∩
(𝐴 × 𝐴)) = (((ℝ*
× ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) |
16 | 14, 15 | eqtri 2765 |
. . . . . 6
⊢ (◡ ≤ ∩ (𝐴 × 𝐴)) = (((ℝ* ×
ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) |
17 | | xpss12 5566 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐴 ⊆
ℝ*) → (𝐴 × 𝐴) ⊆ (ℝ* ×
ℝ*)) |
18 | 17 | anidms 570 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ (𝐴 × 𝐴) ⊆ (ℝ*
× ℝ*)) |
19 | | sseqin2 4130 |
. . . . . . . 8
⊢ ((𝐴 × 𝐴) ⊆ (ℝ* ×
ℝ*) ↔ ((ℝ* × ℝ*)
∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) |
20 | 18, 19 | sylib 221 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ*
→ ((ℝ* × ℝ*) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) |
21 | 20 | difeq1d 4036 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ*
→ (((ℝ* × ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) = ((𝐴 × 𝐴) ∖ < )) |
22 | 16, 21 | eqtr2id 2791 |
. . . . 5
⊢ (𝐴 ⊆ ℝ*
→ ((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴))) |
23 | 22 | adantr 484 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → ((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴))) |
24 | | isoeq2 7127 |
. . . 4
⊢ (((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴)) → (𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
25 | 23, 24 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
26 | 5 | ineq1i 4123 |
. . . . . . 7
⊢ ( ≤
∩ (𝐵 × 𝐵)) = (((ℝ*
× ℝ*) ∖ ◡
< ) ∩ (𝐵 ×
𝐵)) |
27 | | indif1 4186 |
. . . . . . 7
⊢
(((ℝ* × ℝ*) ∖ ◡ < ) ∩ (𝐵 × 𝐵)) = (((ℝ* ×
ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) |
28 | 26, 27 | eqtri 2765 |
. . . . . 6
⊢ ( ≤
∩ (𝐵 × 𝐵)) = (((ℝ*
× ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) |
29 | | xpss12 5566 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐵 × 𝐵) ⊆ (ℝ* ×
ℝ*)) |
30 | 29 | anidms 570 |
. . . . . . . 8
⊢ (𝐵 ⊆ ℝ*
→ (𝐵 × 𝐵) ⊆ (ℝ*
× ℝ*)) |
31 | | sseqin2 4130 |
. . . . . . . 8
⊢ ((𝐵 × 𝐵) ⊆ (ℝ* ×
ℝ*) ↔ ((ℝ* × ℝ*)
∩ (𝐵 × 𝐵)) = (𝐵 × 𝐵)) |
32 | 30, 31 | sylib 221 |
. . . . . . 7
⊢ (𝐵 ⊆ ℝ*
→ ((ℝ* × ℝ*) ∩ (𝐵 × 𝐵)) = (𝐵 × 𝐵)) |
33 | 32 | difeq1d 4036 |
. . . . . 6
⊢ (𝐵 ⊆ ℝ*
→ (((ℝ* × ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) = ((𝐵 × 𝐵) ∖ ◡ < )) |
34 | 28, 33 | eqtr2id 2791 |
. . . . 5
⊢ (𝐵 ⊆ ℝ*
→ ((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵))) |
35 | 34 | adantl 485 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → ((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵))) |
36 | | isoeq3 7128 |
. . . 4
⊢ (((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵)) → (𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
37 | 35, 36 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
38 | 4, 25, 37 | 3bitrd 308 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
39 | | isocnv2 7140 |
. . 3
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ◡◡
≤ , ◡ ≤ (𝐴, 𝐵)) |
40 | | isores2 7142 |
. . . 4
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ◡ ≤ , ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
41 | | isores1 7143 |
. . . 4
⊢ (𝐹 Isom ◡ ≤ , ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
42 | 40, 41 | bitri 278 |
. . 3
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
43 | | lerel 10897 |
. . . . 5
⊢ Rel
≤ |
44 | | dfrel2 6052 |
. . . . 5
⊢ (Rel ≤
↔ ◡◡ ≤ = ≤ ) |
45 | 43, 44 | mpbi 233 |
. . . 4
⊢ ◡◡
≤ = ≤ |
46 | | isoeq2 7127 |
. . . 4
⊢ (◡◡
≤ = ≤ → (𝐹 Isom
◡◡ ≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) |
47 | 45, 46 | ax-mp 5 |
. . 3
⊢ (𝐹 Isom ◡◡
≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵)) |
48 | 39, 42, 47 | 3bitr3ri 305 |
. 2
⊢ (𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
49 | 38, 48 | bitr4di 292 |
1
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) |