Proof of Theorem fpar
Step | Hyp | Ref
| Expression |
1 | | fparlem3 7847 |
. . 3
⊢ (𝐹 Fn 𝐴 → (◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) = ∪
𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V))) |
2 | | fparlem4 7848 |
. . 3
⊢ (𝐺 Fn 𝐵 → (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V)))) = ∪
𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) |
3 | 1, 2 | ineqan12d 4115 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V))))) = (∪ 𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)})))) |
4 | | fpar.1 |
. 2
⊢ 𝐻 = ((◡(1st ↾ (V × V))
∘ (𝐹 ∘
(1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V))
∘ (𝐺 ∘
(2nd ↾ (V × V))))) |
5 | | opex 5332 |
. . . 4
⊢
〈(𝐹‘𝑥), (𝐺‘𝑦)〉 ∈ V |
6 | 5 | dfmpo 7835 |
. . 3
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 {〈〈𝑥, 𝑦〉, 〈(𝐹‘𝑥), (𝐺‘𝑦)〉〉} |
7 | | inxp 5685 |
. . . . . . . 8
⊢ ((({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) = ((({𝑥} × V) ∩ (V × {𝑦})) × (({(𝐹‘𝑥)} × V) ∩ (V × {(𝐺‘𝑦)}))) |
8 | | inxp 5685 |
. . . . . . . . . 10
⊢ (({𝑥} × V) ∩ (V ×
{𝑦})) = (({𝑥} ∩ V) × (V ∩
{𝑦})) |
9 | | inv1 4293 |
. . . . . . . . . . 11
⊢ ({𝑥} ∩ V) = {𝑥} |
10 | | incom 4101 |
. . . . . . . . . . . 12
⊢ (V ∩
{𝑦}) = ({𝑦} ∩ V) |
11 | | inv1 4293 |
. . . . . . . . . . . 12
⊢ ({𝑦} ∩ V) = {𝑦} |
12 | 10, 11 | eqtri 2762 |
. . . . . . . . . . 11
⊢ (V ∩
{𝑦}) = {𝑦} |
13 | 9, 12 | xpeq12i 5563 |
. . . . . . . . . 10
⊢ (({𝑥} ∩ V) × (V ∩
{𝑦})) = ({𝑥} × {𝑦}) |
14 | | vex 3404 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
15 | | vex 3404 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
16 | 14, 15 | xpsn 6925 |
. . . . . . . . . 10
⊢ ({𝑥} × {𝑦}) = {〈𝑥, 𝑦〉} |
17 | 8, 13, 16 | 3eqtri 2766 |
. . . . . . . . 9
⊢ (({𝑥} × V) ∩ (V ×
{𝑦})) = {〈𝑥, 𝑦〉} |
18 | | inxp 5685 |
. . . . . . . . . 10
⊢ (({(𝐹‘𝑥)} × V) ∩ (V × {(𝐺‘𝑦)})) = (({(𝐹‘𝑥)} ∩ V) × (V ∩ {(𝐺‘𝑦)})) |
19 | | inv1 4293 |
. . . . . . . . . . 11
⊢ ({(𝐹‘𝑥)} ∩ V) = {(𝐹‘𝑥)} |
20 | | incom 4101 |
. . . . . . . . . . . 12
⊢ (V ∩
{(𝐺‘𝑦)}) = ({(𝐺‘𝑦)} ∩ V) |
21 | | inv1 4293 |
. . . . . . . . . . . 12
⊢ ({(𝐺‘𝑦)} ∩ V) = {(𝐺‘𝑦)} |
22 | 20, 21 | eqtri 2762 |
. . . . . . . . . . 11
⊢ (V ∩
{(𝐺‘𝑦)}) = {(𝐺‘𝑦)} |
23 | 19, 22 | xpeq12i 5563 |
. . . . . . . . . 10
⊢ (({(𝐹‘𝑥)} ∩ V) × (V ∩ {(𝐺‘𝑦)})) = ({(𝐹‘𝑥)} × {(𝐺‘𝑦)}) |
24 | | fvex 6699 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
25 | | fvex 6699 |
. . . . . . . . . . 11
⊢ (𝐺‘𝑦) ∈ V |
26 | 24, 25 | xpsn 6925 |
. . . . . . . . . 10
⊢ ({(𝐹‘𝑥)} × {(𝐺‘𝑦)}) = {〈(𝐹‘𝑥), (𝐺‘𝑦)〉} |
27 | 18, 23, 26 | 3eqtri 2766 |
. . . . . . . . 9
⊢ (({(𝐹‘𝑥)} × V) ∩ (V × {(𝐺‘𝑦)})) = {〈(𝐹‘𝑥), (𝐺‘𝑦)〉} |
28 | 17, 27 | xpeq12i 5563 |
. . . . . . . 8
⊢ ((({𝑥} × V) ∩ (V ×
{𝑦})) × (({(𝐹‘𝑥)} × V) ∩ (V × {(𝐺‘𝑦)}))) = ({〈𝑥, 𝑦〉} × {〈(𝐹‘𝑥), (𝐺‘𝑦)〉}) |
29 | | opex 5332 |
. . . . . . . . 9
⊢
〈𝑥, 𝑦〉 ∈ V |
30 | 29, 5 | xpsn 6925 |
. . . . . . . 8
⊢
({〈𝑥, 𝑦〉} × {〈(𝐹‘𝑥), (𝐺‘𝑦)〉}) = {〈〈𝑥, 𝑦〉, 〈(𝐹‘𝑥), (𝐺‘𝑦)〉〉} |
31 | 7, 28, 30 | 3eqtri 2766 |
. . . . . . 7
⊢ ((({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) = {〈〈𝑥, 𝑦〉, 〈(𝐹‘𝑥), (𝐺‘𝑦)〉〉} |
32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 → ((({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) = {〈〈𝑥, 𝑦〉, 〈(𝐹‘𝑥), (𝐺‘𝑦)〉〉}) |
33 | 32 | iuneq2i 4912 |
. . . . 5
⊢ ∪ 𝑦 ∈ 𝐵 ((({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) = ∪
𝑦 ∈ 𝐵 {〈〈𝑥, 𝑦〉, 〈(𝐹‘𝑥), (𝐺‘𝑦)〉〉} |
34 | 33 | a1i 11 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → ∪
𝑦 ∈ 𝐵 ((({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) = ∪
𝑦 ∈ 𝐵 {〈〈𝑥, 𝑦〉, 〈(𝐹‘𝑥), (𝐺‘𝑦)〉〉}) |
35 | 34 | iuneq2i 4912 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 ((({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) = ∪
𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 {〈〈𝑥, 𝑦〉, 〈(𝐹‘𝑥), (𝐺‘𝑦)〉〉} |
36 | | 2iunin 4971 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 ((({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) = (∪
𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) |
37 | 6, 35, 36 | 3eqtr2i 2768 |
. 2
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) = (∪ 𝑥 ∈ 𝐴 (({𝑥} × V) × ({(𝐹‘𝑥)} × V)) ∩ ∪ 𝑦 ∈ 𝐵 ((V × {𝑦}) × (V × {(𝐺‘𝑦)}))) |
38 | 3, 4, 37 | 3eqtr4g 2799 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉)) |