Proof of Theorem imainrect
Step | Hyp | Ref
| Expression |
1 | | df-res 4300 |
. . 3
⊢ ((𝐺 ∩ (A × B))
↾ 𝑌) = ((𝐺 ∩ (A × B))
∩ (𝑌 ×
V)) |
2 | 1 | rneqi 4505 |
. 2
⊢ ran
((𝐺 ∩ (A × B))
↾ 𝑌) = ran ((𝐺 ∩ (A × B))
∩ (𝑌 ×
V)) |
3 | | df-ima 4301 |
. 2
⊢ ((𝐺 ∩ (A × B))
“ 𝑌) = ran ((𝐺 ∩ (A × B))
↾ 𝑌) |
4 | | df-ima 4301 |
. . . . 5
⊢ (𝐺 “ (𝑌 ∩ A)) = ran (𝐺 ↾ (𝑌 ∩ A)) |
5 | | df-res 4300 |
. . . . . 6
⊢ (𝐺 ↾ (𝑌 ∩ A)) = (𝐺 ∩ ((𝑌 ∩ A) × V)) |
6 | 5 | rneqi 4505 |
. . . . 5
⊢ ran
(𝐺 ↾ (𝑌 ∩ A)) = ran (𝐺 ∩ ((𝑌 ∩ A) × V)) |
7 | 4, 6 | eqtri 2057 |
. . . 4
⊢ (𝐺 “ (𝑌 ∩ A)) = ran (𝐺 ∩ ((𝑌 ∩ A) × V)) |
8 | 7 | ineq1i 3128 |
. . 3
⊢ ((𝐺 “ (𝑌 ∩ A)) ∩ B) =
(ran (𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ B) |
9 | | cnvin 4674 |
. . . . . 6
⊢ ◡((𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ (V × B)) = (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ ◡(V × B)) |
10 | | inxp 4413 |
. . . . . . . . . 10
⊢
((A × V) ∩ (V ×
B)) = ((A ∩ V) × (V ∩ B)) |
11 | | inv1 3247 |
. . . . . . . . . . 11
⊢ (A ∩ V) = A |
12 | | incom 3123 |
. . . . . . . . . . . 12
⊢ (V ∩
B) = (B
∩ V) |
13 | | inv1 3247 |
. . . . . . . . . . . 12
⊢ (B ∩ V) = B |
14 | 12, 13 | eqtri 2057 |
. . . . . . . . . . 11
⊢ (V ∩
B) = B |
15 | 11, 14 | xpeq12i 4310 |
. . . . . . . . . 10
⊢
((A ∩ V) × (V ∩
B)) = (A × B) |
16 | 10, 15 | eqtr2i 2058 |
. . . . . . . . 9
⊢ (A × B) =
((A × V) ∩ (V × B)) |
17 | 16 | ineq2i 3129 |
. . . . . . . 8
⊢ ((𝐺 ∩ (𝑌 × V)) ∩ (A × B)) =
((𝐺 ∩ (𝑌 × V)) ∩ ((A × V) ∩ (V × B))) |
18 | | in32 3143 |
. . . . . . . 8
⊢ ((𝐺 ∩ (A × B))
∩ (𝑌 × V)) =
((𝐺 ∩ (𝑌 × V)) ∩ (A × B)) |
19 | | xpindir 4415 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∩ A) × V) = ((𝑌 × V) ∩ (A × V)) |
20 | 19 | ineq2i 3129 |
. . . . . . . . . . 11
⊢ (𝐺 ∩ ((𝑌 ∩ A) × V)) = (𝐺 ∩ ((𝑌 × V) ∩ (A × V))) |
21 | | inass 3141 |
. . . . . . . . . . 11
⊢ ((𝐺 ∩ (𝑌 × V)) ∩ (A × V)) = (𝐺 ∩ ((𝑌 × V) ∩ (A × V))) |
22 | 20, 21 | eqtr4i 2060 |
. . . . . . . . . 10
⊢ (𝐺 ∩ ((𝑌 ∩ A) × V)) = ((𝐺 ∩ (𝑌 × V)) ∩ (A × V)) |
23 | 22 | ineq1i 3128 |
. . . . . . . . 9
⊢ ((𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ (V × B)) = (((𝐺 ∩ (𝑌 × V)) ∩ (A × V)) ∩ (V × B)) |
24 | | inass 3141 |
. . . . . . . . 9
⊢ (((𝐺 ∩ (𝑌 × V)) ∩ (A × V)) ∩ (V × B)) = ((𝐺 ∩ (𝑌 × V)) ∩ ((A × V) ∩ (V × B))) |
25 | 23, 24 | eqtri 2057 |
. . . . . . . 8
⊢ ((𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ (V × B)) = ((𝐺 ∩ (𝑌 × V)) ∩ ((A × V) ∩ (V × B))) |
26 | 17, 18, 25 | 3eqtr4i 2067 |
. . . . . . 7
⊢ ((𝐺 ∩ (A × B))
∩ (𝑌 × V)) =
((𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ (V × B)) |
27 | 26 | cnveqi 4453 |
. . . . . 6
⊢ ◡((𝐺 ∩ (A × B))
∩ (𝑌 × V)) =
◡((𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ (V × B)) |
28 | | df-res 4300 |
. . . . . . 7
⊢ (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ↾ B) = (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ (B × V)) |
29 | | cnvxp 4685 |
. . . . . . . 8
⊢ ◡(V × B) = (B ×
V) |
30 | 29 | ineq2i 3129 |
. . . . . . 7
⊢ (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ ◡(V × B)) = (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ (B × V)) |
31 | 28, 30 | eqtr4i 2060 |
. . . . . 6
⊢ (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ↾ B) = (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ ◡(V × B)) |
32 | 9, 27, 31 | 3eqtr4ri 2068 |
. . . . 5
⊢ (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ↾ B) = ◡((𝐺 ∩ (A × B))
∩ (𝑌 ×
V)) |
33 | 32 | dmeqi 4479 |
. . . 4
⊢ dom
(◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ↾ B) = dom ◡((𝐺 ∩ (A × B))
∩ (𝑌 ×
V)) |
34 | | incom 3123 |
. . . . 5
⊢ (B ∩ dom ◡(𝐺 ∩ ((𝑌 ∩ A) × V))) = (dom ◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ B) |
35 | | dmres 4575 |
. . . . 5
⊢ dom
(◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ↾ B) = (B ∩
dom ◡(𝐺 ∩ ((𝑌 ∩ A) × V))) |
36 | | df-rn 4299 |
. . . . . 6
⊢ ran
(𝐺 ∩ ((𝑌 ∩ A) × V)) = dom ◡(𝐺 ∩ ((𝑌 ∩ A) × V)) |
37 | 36 | ineq1i 3128 |
. . . . 5
⊢ (ran
(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ B) = (dom ◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ B) |
38 | 34, 35, 37 | 3eqtr4ri 2068 |
. . . 4
⊢ (ran
(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ B) = dom (◡(𝐺 ∩ ((𝑌 ∩ A) × V)) ↾ B) |
39 | | df-rn 4299 |
. . . 4
⊢ ran
((𝐺 ∩ (A × B))
∩ (𝑌 × V)) = dom
◡((𝐺 ∩ (A × B))
∩ (𝑌 ×
V)) |
40 | 33, 38, 39 | 3eqtr4ri 2068 |
. . 3
⊢ ran
((𝐺 ∩ (A × B))
∩ (𝑌 × V)) = (ran
(𝐺 ∩ ((𝑌 ∩ A) × V)) ∩ B) |
41 | 8, 40 | eqtr4i 2060 |
. 2
⊢ ((𝐺 “ (𝑌 ∩ A)) ∩ B) =
ran ((𝐺 ∩ (A × B))
∩ (𝑌 ×
V)) |
42 | 2, 3, 41 | 3eqtr4i 2067 |
1
⊢ ((𝐺 ∩ (A × B))
“ 𝑌) = ((𝐺 “ (𝑌 ∩ A)) ∩ B) |