Proof of Theorem imainrect
Step | Hyp | Ref
| Expression |
1 | | df-res 4611 |
. . 3
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) ↾ 𝑌) = ((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) |
2 | 1 | rneqi 4827 |
. 2
⊢ ran
((𝐺 ∩ (𝐴 × 𝐵)) ↾ 𝑌) = ran ((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) |
3 | | df-ima 4612 |
. 2
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ran ((𝐺 ∩ (𝐴 × 𝐵)) ↾ 𝑌) |
4 | | df-ima 4612 |
. . . . 5
⊢ (𝐺 “ (𝑌 ∩ 𝐴)) = ran (𝐺 ↾ (𝑌 ∩ 𝐴)) |
5 | | df-res 4611 |
. . . . . 6
⊢ (𝐺 ↾ (𝑌 ∩ 𝐴)) = (𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) |
6 | 5 | rneqi 4827 |
. . . . 5
⊢ ran
(𝐺 ↾ (𝑌 ∩ 𝐴)) = ran (𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) |
7 | 4, 6 | eqtri 2185 |
. . . 4
⊢ (𝐺 “ (𝑌 ∩ 𝐴)) = ran (𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) |
8 | 7 | ineq1i 3315 |
. . 3
⊢ ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) = (ran (𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ 𝐵) |
9 | | cnvin 5006 |
. . . . . 6
⊢ ◡((𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ (V × 𝐵)) = (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ ◡(V × 𝐵)) |
10 | | inxp 4733 |
. . . . . . . . . 10
⊢ ((𝐴 × V) ∩ (V ×
𝐵)) = ((𝐴 ∩ V) × (V ∩ 𝐵)) |
11 | | inv1 3441 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ V) = 𝐴 |
12 | | incom 3310 |
. . . . . . . . . . . 12
⊢ (V ∩
𝐵) = (𝐵 ∩ V) |
13 | | inv1 3441 |
. . . . . . . . . . . 12
⊢ (𝐵 ∩ V) = 𝐵 |
14 | 12, 13 | eqtri 2185 |
. . . . . . . . . . 11
⊢ (V ∩
𝐵) = 𝐵 |
15 | 11, 14 | xpeq12i 4621 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ V) × (V ∩ 𝐵)) = (𝐴 × 𝐵) |
16 | 10, 15 | eqtr2i 2186 |
. . . . . . . . 9
⊢ (𝐴 × 𝐵) = ((𝐴 × V) ∩ (V × 𝐵)) |
17 | 16 | ineq2i 3316 |
. . . . . . . 8
⊢ ((𝐺 ∩ (𝑌 × V)) ∩ (𝐴 × 𝐵)) = ((𝐺 ∩ (𝑌 × V)) ∩ ((𝐴 × V) ∩ (V × 𝐵))) |
18 | | in32 3330 |
. . . . . . . 8
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) = ((𝐺 ∩ (𝑌 × V)) ∩ (𝐴 × 𝐵)) |
19 | | xpindir 4735 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∩ 𝐴) × V) = ((𝑌 × V) ∩ (𝐴 × V)) |
20 | 19 | ineq2i 3316 |
. . . . . . . . . . 11
⊢ (𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) = (𝐺 ∩ ((𝑌 × V) ∩ (𝐴 × V))) |
21 | | inass 3328 |
. . . . . . . . . . 11
⊢ ((𝐺 ∩ (𝑌 × V)) ∩ (𝐴 × V)) = (𝐺 ∩ ((𝑌 × V) ∩ (𝐴 × V))) |
22 | 20, 21 | eqtr4i 2188 |
. . . . . . . . . 10
⊢ (𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) = ((𝐺 ∩ (𝑌 × V)) ∩ (𝐴 × V)) |
23 | 22 | ineq1i 3315 |
. . . . . . . . 9
⊢ ((𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ (V × 𝐵)) = (((𝐺 ∩ (𝑌 × V)) ∩ (𝐴 × V)) ∩ (V × 𝐵)) |
24 | | inass 3328 |
. . . . . . . . 9
⊢ (((𝐺 ∩ (𝑌 × V)) ∩ (𝐴 × V)) ∩ (V × 𝐵)) = ((𝐺 ∩ (𝑌 × V)) ∩ ((𝐴 × V) ∩ (V × 𝐵))) |
25 | 23, 24 | eqtri 2185 |
. . . . . . . 8
⊢ ((𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ (V × 𝐵)) = ((𝐺 ∩ (𝑌 × V)) ∩ ((𝐴 × V) ∩ (V × 𝐵))) |
26 | 17, 18, 25 | 3eqtr4i 2195 |
. . . . . . 7
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) = ((𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ (V × 𝐵)) |
27 | 26 | cnveqi 4774 |
. . . . . 6
⊢ ◡((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) = ◡((𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ (V × 𝐵)) |
28 | | df-res 4611 |
. . . . . . 7
⊢ (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ↾ 𝐵) = (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ (𝐵 × V)) |
29 | | cnvxp 5017 |
. . . . . . . 8
⊢ ◡(V × 𝐵) = (𝐵 × V) |
30 | 29 | ineq2i 3316 |
. . . . . . 7
⊢ (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ ◡(V × 𝐵)) = (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ (𝐵 × V)) |
31 | 28, 30 | eqtr4i 2188 |
. . . . . 6
⊢ (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ↾ 𝐵) = (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ ◡(V × 𝐵)) |
32 | 9, 27, 31 | 3eqtr4ri 2196 |
. . . . 5
⊢ (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ↾ 𝐵) = ◡((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) |
33 | 32 | dmeqi 4800 |
. . . 4
⊢ dom
(◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ↾ 𝐵) = dom ◡((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) |
34 | | incom 3310 |
. . . . 5
⊢ (𝐵 ∩ dom ◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V))) = (dom ◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ 𝐵) |
35 | | dmres 4900 |
. . . . 5
⊢ dom
(◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ↾ 𝐵) = (𝐵 ∩ dom ◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V))) |
36 | | df-rn 4610 |
. . . . . 6
⊢ ran
(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) = dom ◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) |
37 | 36 | ineq1i 3315 |
. . . . 5
⊢ (ran
(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ 𝐵) = (dom ◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ 𝐵) |
38 | 34, 35, 37 | 3eqtr4ri 2196 |
. . . 4
⊢ (ran
(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ 𝐵) = dom (◡(𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ↾ 𝐵) |
39 | | df-rn 4610 |
. . . 4
⊢ ran
((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) = dom ◡((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) |
40 | 33, 38, 39 | 3eqtr4ri 2196 |
. . 3
⊢ ran
((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) = (ran (𝐺 ∩ ((𝑌 ∩ 𝐴) × V)) ∩ 𝐵) |
41 | 8, 40 | eqtr4i 2188 |
. 2
⊢ ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) = ran ((𝐺 ∩ (𝐴 × 𝐵)) ∩ (𝑌 × V)) |
42 | 2, 3, 41 | 3eqtr4i 2195 |
1
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) |