Proof of Theorem gtiso
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢ ((𝐴 × 𝐴) ∖ < ) = ((𝐴 × 𝐴) ∖ < ) |
| 2 | | eqid 2737 |
. . . . 5
⊢ ((𝐵 × 𝐵) ∖ ◡ < ) = ((𝐵 × 𝐵) ∖ ◡ < ) |
| 3 | 1, 2 | isocnv3 7352 |
. . . 4
⊢ (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵)) |
| 4 | 3 | a1i 11 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
| 5 | | df-le 11301 |
. . . . . . . . . 10
⊢ ≤ =
((ℝ* × ℝ*) ∖ ◡ < ) |
| 6 | 5 | cnveqi 5885 |
. . . . . . . . 9
⊢ ◡ ≤ = ◡((ℝ* ×
ℝ*) ∖ ◡ <
) |
| 7 | | cnvdif 6163 |
. . . . . . . . 9
⊢ ◡((ℝ* ×
ℝ*) ∖ ◡ < ) =
(◡(ℝ* ×
ℝ*) ∖ ◡◡ < ) |
| 8 | | cnvxp 6177 |
. . . . . . . . . 10
⊢ ◡(ℝ* ×
ℝ*) = (ℝ* ×
ℝ*) |
| 9 | | ltrel 11323 |
. . . . . . . . . . 11
⊢ Rel
< |
| 10 | | dfrel2 6209 |
. . . . . . . . . . 11
⊢ (Rel <
↔ ◡◡ < = < ) |
| 11 | 9, 10 | mpbi 230 |
. . . . . . . . . 10
⊢ ◡◡
< = < |
| 12 | 8, 11 | difeq12i 4124 |
. . . . . . . . 9
⊢ (◡(ℝ* ×
ℝ*) ∖ ◡◡ < ) = ((ℝ* ×
ℝ*) ∖ < ) |
| 13 | 6, 7, 12 | 3eqtri 2769 |
. . . . . . . 8
⊢ ◡ ≤ = ((ℝ* ×
ℝ*) ∖ < ) |
| 14 | 13 | ineq1i 4216 |
. . . . . . 7
⊢ (◡ ≤ ∩ (𝐴 × 𝐴)) = (((ℝ* ×
ℝ*) ∖ < ) ∩ (𝐴 × 𝐴)) |
| 15 | | indif1 4282 |
. . . . . . 7
⊢
(((ℝ* × ℝ*) ∖ < ) ∩
(𝐴 × 𝐴)) = (((ℝ*
× ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) |
| 16 | 14, 15 | eqtri 2765 |
. . . . . 6
⊢ (◡ ≤ ∩ (𝐴 × 𝐴)) = (((ℝ* ×
ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) |
| 17 | | xpss12 5700 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐴 ⊆
ℝ*) → (𝐴 × 𝐴) ⊆ (ℝ* ×
ℝ*)) |
| 18 | 17 | anidms 566 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ (𝐴 × 𝐴) ⊆ (ℝ*
× ℝ*)) |
| 19 | | sseqin2 4223 |
. . . . . . . 8
⊢ ((𝐴 × 𝐴) ⊆ (ℝ* ×
ℝ*) ↔ ((ℝ* × ℝ*)
∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) |
| 20 | 18, 19 | sylib 218 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ*
→ ((ℝ* × ℝ*) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴)) |
| 21 | 20 | difeq1d 4125 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ*
→ (((ℝ* × ℝ*) ∩ (𝐴 × 𝐴)) ∖ < ) = ((𝐴 × 𝐴) ∖ < )) |
| 22 | 16, 21 | eqtr2id 2790 |
. . . . 5
⊢ (𝐴 ⊆ ℝ*
→ ((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴))) |
| 23 | 22 | adantr 480 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → ((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴))) |
| 24 | | isoeq2 7338 |
. . . 4
⊢ (((𝐴 × 𝐴) ∖ < ) = (◡ ≤ ∩ (𝐴 × 𝐴)) → (𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
| 25 | 23, 24 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom ((𝐴 × 𝐴) ∖ < ), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵))) |
| 26 | 5 | ineq1i 4216 |
. . . . . . 7
⊢ ( ≤
∩ (𝐵 × 𝐵)) = (((ℝ*
× ℝ*) ∖ ◡
< ) ∩ (𝐵 ×
𝐵)) |
| 27 | | indif1 4282 |
. . . . . . 7
⊢
(((ℝ* × ℝ*) ∖ ◡ < ) ∩ (𝐵 × 𝐵)) = (((ℝ* ×
ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) |
| 28 | 26, 27 | eqtri 2765 |
. . . . . 6
⊢ ( ≤
∩ (𝐵 × 𝐵)) = (((ℝ*
× ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) |
| 29 | | xpss12 5700 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐵 × 𝐵) ⊆ (ℝ* ×
ℝ*)) |
| 30 | 29 | anidms 566 |
. . . . . . . 8
⊢ (𝐵 ⊆ ℝ*
→ (𝐵 × 𝐵) ⊆ (ℝ*
× ℝ*)) |
| 31 | | sseqin2 4223 |
. . . . . . . 8
⊢ ((𝐵 × 𝐵) ⊆ (ℝ* ×
ℝ*) ↔ ((ℝ* × ℝ*)
∩ (𝐵 × 𝐵)) = (𝐵 × 𝐵)) |
| 32 | 30, 31 | sylib 218 |
. . . . . . 7
⊢ (𝐵 ⊆ ℝ*
→ ((ℝ* × ℝ*) ∩ (𝐵 × 𝐵)) = (𝐵 × 𝐵)) |
| 33 | 32 | difeq1d 4125 |
. . . . . 6
⊢ (𝐵 ⊆ ℝ*
→ (((ℝ* × ℝ*) ∩ (𝐵 × 𝐵)) ∖ ◡ < ) = ((𝐵 × 𝐵) ∖ ◡ < )) |
| 34 | 28, 33 | eqtr2id 2790 |
. . . . 5
⊢ (𝐵 ⊆ ℝ*
→ ((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵))) |
| 35 | 34 | adantl 481 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → ((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵))) |
| 36 | | isoeq3 7339 |
. . . 4
⊢ (((𝐵 × 𝐵) ∖ ◡ < ) = ( ≤ ∩ (𝐵 × 𝐵)) → (𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
| 37 | 35, 36 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ((𝐵 × 𝐵) ∖ ◡ < )(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
| 38 | 4, 25, 37 | 3bitrd 305 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵))) |
| 39 | | isocnv2 7351 |
. . 3
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ◡◡
≤ , ◡ ≤ (𝐴, 𝐵)) |
| 40 | | isores2 7353 |
. . . 4
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ◡ ≤ , ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
| 41 | | isores1 7354 |
. . . 4
⊢ (𝐹 Isom ◡ ≤ , ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
| 42 | 40, 41 | bitri 275 |
. . 3
⊢ (𝐹 Isom ◡ ≤ , ≤ (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
| 43 | | lerel 11325 |
. . . . 5
⊢ Rel
≤ |
| 44 | | dfrel2 6209 |
. . . . 5
⊢ (Rel ≤
↔ ◡◡ ≤ = ≤ ) |
| 45 | 43, 44 | mpbi 230 |
. . . 4
⊢ ◡◡
≤ = ≤ |
| 46 | | isoeq2 7338 |
. . . 4
⊢ (◡◡
≤ = ≤ → (𝐹 Isom
◡◡ ≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) |
| 47 | 45, 46 | ax-mp 5 |
. . 3
⊢ (𝐹 Isom ◡◡
≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵)) |
| 48 | 39, 42, 47 | 3bitr3ri 302 |
. 2
⊢ (𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵) ↔ 𝐹 Isom (◡ ≤ ∩ (𝐴 × 𝐴)), ( ≤ ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) |
| 49 | 38, 48 | bitr4di 289 |
1
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐵 ⊆
ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) |