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 ≤ , ◡ ≤ ( 𝐴 , 𝐵 ) ) ) |