Step | Hyp | Ref
| Expression |
1 | | fparlem3 8051 |
. . 3
β’ (πΉ Fn π΄ β (β‘(1st βΎ (V Γ V))
β (πΉ β
(1st βΎ (V Γ V)))) = βͺ
π₯ β π΄ (({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V))) |
2 | | fparlem4 8052 |
. . 3
β’ (πΊ Fn π΅ β (β‘(2nd βΎ (V Γ V))
β (πΊ β
(2nd βΎ (V Γ V)))) = βͺ
π¦ β π΅ ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) |
3 | 1, 2 | ineqan12d 4179 |
. 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 5426 |
. . . 4
β’
β¨(πΉβπ₯), (πΊβπ¦)β© β V |
6 | 5 | dfmpo 8039 |
. . 3
β’ (π₯ β π΄, π¦ β π΅ β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) = βͺ π₯ β π΄ βͺ π¦ β π΅ {β¨β¨π₯, π¦β©, β¨(πΉβπ₯), (πΊβπ¦)β©β©} |
7 | | inxp 5793 |
. . . . . . . 8
β’ ((({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) = ((({π₯} Γ V) β© (V Γ {π¦})) Γ (({(πΉβπ₯)} Γ V) β© (V Γ {(πΊβπ¦)}))) |
8 | | inxp 5793 |
. . . . . . . . . 10
β’ (({π₯} Γ V) β© (V Γ
{π¦})) = (({π₯} β© V) Γ (V β©
{π¦})) |
9 | | inv1 4359 |
. . . . . . . . . . 11
β’ ({π₯} β© V) = {π₯} |
10 | | incom 4166 |
. . . . . . . . . . . 12
β’ (V β©
{π¦}) = ({π¦} β© V) |
11 | | inv1 4359 |
. . . . . . . . . . . 12
β’ ({π¦} β© V) = {π¦} |
12 | 10, 11 | eqtri 2765 |
. . . . . . . . . . 11
β’ (V β©
{π¦}) = {π¦} |
13 | 9, 12 | xpeq12i 5666 |
. . . . . . . . . 10
β’ (({π₯} β© V) Γ (V β©
{π¦})) = ({π₯} Γ {π¦}) |
14 | | vex 3452 |
. . . . . . . . . . 11
β’ π₯ β V |
15 | | vex 3452 |
. . . . . . . . . . 11
β’ π¦ β V |
16 | 14, 15 | xpsn 7092 |
. . . . . . . . . 10
β’ ({π₯} Γ {π¦}) = {β¨π₯, π¦β©} |
17 | 8, 13, 16 | 3eqtri 2769 |
. . . . . . . . 9
β’ (({π₯} Γ V) β© (V Γ
{π¦})) = {β¨π₯, π¦β©} |
18 | | inxp 5793 |
. . . . . . . . . 10
β’ (({(πΉβπ₯)} Γ V) β© (V Γ {(πΊβπ¦)})) = (({(πΉβπ₯)} β© V) Γ (V β© {(πΊβπ¦)})) |
19 | | inv1 4359 |
. . . . . . . . . . 11
β’ ({(πΉβπ₯)} β© V) = {(πΉβπ₯)} |
20 | | incom 4166 |
. . . . . . . . . . . 12
β’ (V β©
{(πΊβπ¦)}) = ({(πΊβπ¦)} β© V) |
21 | | inv1 4359 |
. . . . . . . . . . . 12
β’ ({(πΊβπ¦)} β© V) = {(πΊβπ¦)} |
22 | 20, 21 | eqtri 2765 |
. . . . . . . . . . 11
β’ (V β©
{(πΊβπ¦)}) = {(πΊβπ¦)} |
23 | 19, 22 | xpeq12i 5666 |
. . . . . . . . . 10
β’ (({(πΉβπ₯)} β© V) Γ (V β© {(πΊβπ¦)})) = ({(πΉβπ₯)} Γ {(πΊβπ¦)}) |
24 | | fvex 6860 |
. . . . . . . . . . 11
β’ (πΉβπ₯) β V |
25 | | fvex 6860 |
. . . . . . . . . . 11
β’ (πΊβπ¦) β V |
26 | 24, 25 | xpsn 7092 |
. . . . . . . . . 10
β’ ({(πΉβπ₯)} Γ {(πΊβπ¦)}) = {β¨(πΉβπ₯), (πΊβπ¦)β©} |
27 | 18, 23, 26 | 3eqtri 2769 |
. . . . . . . . 9
β’ (({(πΉβπ₯)} Γ V) β© (V Γ {(πΊβπ¦)})) = {β¨(πΉβπ₯), (πΊβπ¦)β©} |
28 | 17, 27 | xpeq12i 5666 |
. . . . . . . 8
β’ ((({π₯} Γ V) β© (V Γ
{π¦})) Γ (({(πΉβπ₯)} Γ V) β© (V Γ {(πΊβπ¦)}))) = ({β¨π₯, π¦β©} Γ {β¨(πΉβπ₯), (πΊβπ¦)β©}) |
29 | | opex 5426 |
. . . . . . . . 9
β’
β¨π₯, π¦β© β V |
30 | 29, 5 | xpsn 7092 |
. . . . . . . 8
β’
({β¨π₯, π¦β©} Γ {β¨(πΉβπ₯), (πΊβπ¦)β©}) = {β¨β¨π₯, π¦β©, β¨(πΉβπ₯), (πΊβπ¦)β©β©} |
31 | 7, 28, 30 | 3eqtri 2769 |
. . . . . . 7
β’ ((({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) = {β¨β¨π₯, π¦β©, β¨(πΉβπ₯), (πΊβπ¦)β©β©} |
32 | 31 | a1i 11 |
. . . . . 6
β’ (π¦ β π΅ β ((({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) = {β¨β¨π₯, π¦β©, β¨(πΉβπ₯), (πΊβπ¦)β©β©}) |
33 | 32 | iuneq2i 4980 |
. . . . 5
β’ βͺ π¦ β π΅ ((({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) = βͺ
π¦ β π΅ {β¨β¨π₯, π¦β©, β¨(πΉβπ₯), (πΊβπ¦)β©β©} |
34 | 33 | a1i 11 |
. . . 4
β’ (π₯ β π΄ β βͺ
π¦ β π΅ ((({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) = βͺ
π¦ β π΅ {β¨β¨π₯, π¦β©, β¨(πΉβπ₯), (πΊβπ¦)β©β©}) |
35 | 34 | iuneq2i 4980 |
. . 3
β’ βͺ π₯ β π΄ βͺ π¦ β π΅ ((({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) = βͺ
π₯ β π΄ βͺ π¦ β π΅ {β¨β¨π₯, π¦β©, β¨(πΉβπ₯), (πΊβπ¦)β©β©} |
36 | | 2iunin 5041 |
. . 3
β’ βͺ π₯ β π΄ βͺ π¦ β π΅ ((({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) = (βͺ
π₯ β π΄ (({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© βͺ π¦ β π΅ ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) |
37 | 6, 35, 36 | 3eqtr2i 2771 |
. 2
β’ (π₯ β π΄, π¦ β π΅ β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) = (βͺ π₯ β π΄ (({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V)) β© βͺ π¦ β π΅ ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) |
38 | 3, 4, 37 | 3eqtr4g 2802 |
1
β’ ((πΉ Fn π΄ β§ πΊ Fn π΅) β π» = (π₯ β π΄, π¦ β π΅ β¦ β¨(πΉβπ₯), (πΊβπ¦)β©)) |