Step | Hyp | Ref
| Expression |
1 | | ptunhmeo.g |
. . . 4
β’ πΊ = (π₯ β π, π¦ β π β¦ (π₯ βͺ π¦)) |
2 | | vex 3479 |
. . . . . . 7
β’ π₯ β V |
3 | | vex 3479 |
. . . . . . 7
β’ π¦ β V |
4 | 2, 3 | op1std 7985 |
. . . . . 6
β’ (π€ = β¨π₯, π¦β© β (1st βπ€) = π₯) |
5 | 2, 3 | op2ndd 7986 |
. . . . . 6
β’ (π€ = β¨π₯, π¦β© β (2nd βπ€) = π¦) |
6 | 4, 5 | uneq12d 4165 |
. . . . 5
β’ (π€ = β¨π₯, π¦β© β ((1st βπ€) βͺ (2nd
βπ€)) = (π₯ βͺ π¦)) |
7 | 6 | mpompt 7522 |
. . . 4
β’ (π€ β (π Γ π) β¦ ((1st βπ€) βͺ (2nd
βπ€))) = (π₯ β π, π¦ β π β¦ (π₯ βͺ π¦)) |
8 | 1, 7 | eqtr4i 2764 |
. . 3
β’ πΊ = (π€ β (π Γ π) β¦ ((1st βπ€) βͺ (2nd
βπ€))) |
9 | | xp1st 8007 |
. . . . . . 7
β’ (π€ β (π Γ π) β (1st βπ€) β π) |
10 | 9 | adantl 483 |
. . . . . 6
β’ ((π β§ π€ β (π Γ π)) β (1st βπ€) β π) |
11 | | ixpeq2 8905 |
. . . . . . . . . 10
β’
(βπ β
π΄ βͺ ((πΉ
βΎ π΄)βπ) = βͺ
(πΉβπ) β Xπ β π΄ βͺ ((πΉ βΎ π΄)βπ) = Xπ β π΄ βͺ (πΉβπ)) |
12 | | fvres 6911 |
. . . . . . . . . . 11
β’ (π β π΄ β ((πΉ βΎ π΄)βπ) = (πΉβπ)) |
13 | 12 | unieqd 4923 |
. . . . . . . . . 10
β’ (π β π΄ β βͺ ((πΉ βΎ π΄)βπ) = βͺ (πΉβπ)) |
14 | 11, 13 | mprg 3068 |
. . . . . . . . 9
β’ Xπ β
π΄ βͺ ((πΉ
βΎ π΄)βπ) = Xπ β
π΄ βͺ (πΉβπ) |
15 | | ptunhmeo.c |
. . . . . . . . . . 11
β’ (π β πΆ β π) |
16 | | ssun1 4173 |
. . . . . . . . . . . 12
β’ π΄ β (π΄ βͺ π΅) |
17 | | ptunhmeo.u |
. . . . . . . . . . . 12
β’ (π β πΆ = (π΄ βͺ π΅)) |
18 | 16, 17 | sseqtrrid 4036 |
. . . . . . . . . . 11
β’ (π β π΄ β πΆ) |
19 | 15, 18 | ssexd 5325 |
. . . . . . . . . 10
β’ (π β π΄ β V) |
20 | | ptunhmeo.f |
. . . . . . . . . . 11
β’ (π β πΉ:πΆβΆTop) |
21 | 20, 18 | fssresd 6759 |
. . . . . . . . . 10
β’ (π β (πΉ βΎ π΄):π΄βΆTop) |
22 | | ptunhmeo.k |
. . . . . . . . . . 11
β’ πΎ =
(βtβ(πΉ βΎ π΄)) |
23 | 22 | ptuni 23098 |
. . . . . . . . . 10
β’ ((π΄ β V β§ (πΉ βΎ π΄):π΄βΆTop) β Xπ β
π΄ βͺ ((πΉ
βΎ π΄)βπ) = βͺ
πΎ) |
24 | 19, 21, 23 | syl2anc 585 |
. . . . . . . . 9
β’ (π β Xπ β
π΄ βͺ ((πΉ
βΎ π΄)βπ) = βͺ
πΎ) |
25 | 14, 24 | eqtr3id 2787 |
. . . . . . . 8
β’ (π β Xπ β
π΄ βͺ (πΉβπ) = βͺ πΎ) |
26 | | ptunhmeo.x |
. . . . . . . 8
β’ π = βͺ
πΎ |
27 | 25, 26 | eqtr4di 2791 |
. . . . . . 7
β’ (π β Xπ β
π΄ βͺ (πΉβπ) = π) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ π€ β (π Γ π)) β Xπ β π΄ βͺ (πΉβπ) = π) |
29 | 10, 28 | eleqtrrd 2837 |
. . . . 5
β’ ((π β§ π€ β (π Γ π)) β (1st βπ€) β Xπ β
π΄ βͺ (πΉβπ)) |
30 | | xp2nd 8008 |
. . . . . . 7
β’ (π€ β (π Γ π) β (2nd βπ€) β π) |
31 | 30 | adantl 483 |
. . . . . 6
β’ ((π β§ π€ β (π Γ π)) β (2nd βπ€) β π) |
32 | 17 | eqcomd 2739 |
. . . . . . . . . 10
β’ (π β (π΄ βͺ π΅) = πΆ) |
33 | | ptunhmeo.i |
. . . . . . . . . . 11
β’ (π β (π΄ β© π΅) = β
) |
34 | | uneqdifeq 4493 |
. . . . . . . . . . 11
β’ ((π΄ β πΆ β§ (π΄ β© π΅) = β
) β ((π΄ βͺ π΅) = πΆ β (πΆ β π΄) = π΅)) |
35 | 18, 33, 34 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β ((π΄ βͺ π΅) = πΆ β (πΆ β π΄) = π΅)) |
36 | 32, 35 | mpbid 231 |
. . . . . . . . 9
β’ (π β (πΆ β π΄) = π΅) |
37 | 36 | ixpeq1d 8903 |
. . . . . . . 8
β’ (π β Xπ β
(πΆ β π΄)βͺ
(πΉβπ) = Xπ β π΅ βͺ (πΉβπ)) |
38 | | ixpeq2 8905 |
. . . . . . . . . . 11
β’
(βπ β
π΅ βͺ ((πΉ
βΎ π΅)βπ) = βͺ
(πΉβπ) β Xπ β π΅ βͺ ((πΉ βΎ π΅)βπ) = Xπ β π΅ βͺ (πΉβπ)) |
39 | | fvres 6911 |
. . . . . . . . . . . 12
β’ (π β π΅ β ((πΉ βΎ π΅)βπ) = (πΉβπ)) |
40 | 39 | unieqd 4923 |
. . . . . . . . . . 11
β’ (π β π΅ β βͺ ((πΉ βΎ π΅)βπ) = βͺ (πΉβπ)) |
41 | 38, 40 | mprg 3068 |
. . . . . . . . . 10
β’ Xπ β
π΅ βͺ ((πΉ
βΎ π΅)βπ) = Xπ β
π΅ βͺ (πΉβπ) |
42 | | ssun2 4174 |
. . . . . . . . . . . . 13
β’ π΅ β (π΄ βͺ π΅) |
43 | 42, 17 | sseqtrrid 4036 |
. . . . . . . . . . . 12
β’ (π β π΅ β πΆ) |
44 | 15, 43 | ssexd 5325 |
. . . . . . . . . . 11
β’ (π β π΅ β V) |
45 | 20, 43 | fssresd 6759 |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ π΅):π΅βΆTop) |
46 | | ptunhmeo.l |
. . . . . . . . . . . 12
β’ πΏ =
(βtβ(πΉ βΎ π΅)) |
47 | 46 | ptuni 23098 |
. . . . . . . . . . 11
β’ ((π΅ β V β§ (πΉ βΎ π΅):π΅βΆTop) β Xπ β
π΅ βͺ ((πΉ
βΎ π΅)βπ) = βͺ
πΏ) |
48 | 44, 45, 47 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β Xπ β
π΅ βͺ ((πΉ
βΎ π΅)βπ) = βͺ
πΏ) |
49 | 41, 48 | eqtr3id 2787 |
. . . . . . . . 9
β’ (π β Xπ β
π΅ βͺ (πΉβπ) = βͺ πΏ) |
50 | | ptunhmeo.y |
. . . . . . . . 9
β’ π = βͺ
πΏ |
51 | 49, 50 | eqtr4di 2791 |
. . . . . . . 8
β’ (π β Xπ β
π΅ βͺ (πΉβπ) = π) |
52 | 37, 51 | eqtrd 2773 |
. . . . . . 7
β’ (π β Xπ β
(πΆ β π΄)βͺ
(πΉβπ) = π) |
53 | 52 | adantr 482 |
. . . . . 6
β’ ((π β§ π€ β (π Γ π)) β Xπ β (πΆ β π΄)βͺ (πΉβπ) = π) |
54 | 31, 53 | eleqtrrd 2837 |
. . . . 5
β’ ((π β§ π€ β (π Γ π)) β (2nd βπ€) β Xπ β
(πΆ β π΄)βͺ
(πΉβπ)) |
55 | 18 | adantr 482 |
. . . . 5
β’ ((π β§ π€ β (π Γ π)) β π΄ β πΆ) |
56 | | undifixp 8928 |
. . . . 5
β’
(((1st βπ€) β Xπ β π΄ βͺ (πΉβπ) β§ (2nd βπ€) β Xπ β
(πΆ β π΄)βͺ
(πΉβπ) β§ π΄ β πΆ) β ((1st βπ€) βͺ (2nd
βπ€)) β Xπ β
πΆ βͺ (πΉβπ)) |
57 | 29, 54, 55, 56 | syl3anc 1372 |
. . . 4
β’ ((π β§ π€ β (π Γ π)) β ((1st βπ€) βͺ (2nd
βπ€)) β Xπ β
πΆ βͺ (πΉβπ)) |
58 | | ptunhmeo.j |
. . . . . . 7
β’ π½ =
(βtβπΉ) |
59 | 58 | ptuni 23098 |
. . . . . 6
β’ ((πΆ β π β§ πΉ:πΆβΆTop) β Xπ β
πΆ βͺ (πΉβπ) = βͺ π½) |
60 | 15, 20, 59 | syl2anc 585 |
. . . . 5
β’ (π β Xπ β
πΆ βͺ (πΉβπ) = βͺ π½) |
61 | 60 | adantr 482 |
. . . 4
β’ ((π β§ π€ β (π Γ π)) β Xπ β πΆ βͺ (πΉβπ) = βͺ π½) |
62 | 57, 61 | eleqtrd 2836 |
. . 3
β’ ((π β§ π€ β (π Γ π)) β ((1st βπ€) βͺ (2nd
βπ€)) β βͺ π½) |
63 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β βͺ π½) β π΄ β πΆ) |
64 | 60 | eleq2d 2820 |
. . . . . . 7
β’ (π β (π§ β Xπ β πΆ βͺ (πΉβπ) β π§ β βͺ π½)) |
65 | 64 | biimpar 479 |
. . . . . 6
β’ ((π β§ π§ β βͺ π½) β π§ β Xπ β πΆ βͺ (πΉβπ)) |
66 | | resixp 8927 |
. . . . . 6
β’ ((π΄ β πΆ β§ π§ β Xπ β πΆ βͺ (πΉβπ)) β (π§ βΎ π΄) β Xπ β π΄ βͺ (πΉβπ)) |
67 | 63, 65, 66 | syl2anc 585 |
. . . . 5
β’ ((π β§ π§ β βͺ π½) β (π§ βΎ π΄) β Xπ β π΄ βͺ (πΉβπ)) |
68 | 27 | adantr 482 |
. . . . 5
β’ ((π β§ π§ β βͺ π½) β Xπ β
π΄ βͺ (πΉβπ) = π) |
69 | 67, 68 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π§ β βͺ π½) β (π§ βΎ π΄) β π) |
70 | 43 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β βͺ π½) β π΅ β πΆ) |
71 | | resixp 8927 |
. . . . . 6
β’ ((π΅ β πΆ β§ π§ β Xπ β πΆ βͺ (πΉβπ)) β (π§ βΎ π΅) β Xπ β π΅ βͺ (πΉβπ)) |
72 | 70, 65, 71 | syl2anc 585 |
. . . . 5
β’ ((π β§ π§ β βͺ π½) β (π§ βΎ π΅) β Xπ β π΅ βͺ (πΉβπ)) |
73 | 51 | adantr 482 |
. . . . 5
β’ ((π β§ π§ β βͺ π½) β Xπ β
π΅ βͺ (πΉβπ) = π) |
74 | 72, 73 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π§ β βͺ π½) β (π§ βΎ π΅) β π) |
75 | 69, 74 | opelxpd 5716 |
. . 3
β’ ((π β§ π§ β βͺ π½) β β¨(π§ βΎ π΄), (π§ βΎ π΅)β© β (π Γ π)) |
76 | | eqop 8017 |
. . . . 5
β’ (π€ β (π Γ π) β (π€ = β¨(π§ βΎ π΄), (π§ βΎ π΅)β© β ((1st βπ€) = (π§ βΎ π΄) β§ (2nd βπ€) = (π§ βΎ π΅)))) |
77 | 76 | ad2antrl 727 |
. . . 4
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (π€ = β¨(π§ βΎ π΄), (π§ βΎ π΅)β© β ((1st βπ€) = (π§ βΎ π΄) β§ (2nd βπ€) = (π§ βΎ π΅)))) |
78 | 65 | adantrl 715 |
. . . . . . . . 9
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β π§ β Xπ β πΆ βͺ (πΉβπ)) |
79 | | ixpfn 8897 |
. . . . . . . . 9
β’ (π§ β Xπ β
πΆ βͺ (πΉβπ) β π§ Fn πΆ) |
80 | | fnresdm 6670 |
. . . . . . . . 9
β’ (π§ Fn πΆ β (π§ βΎ πΆ) = π§) |
81 | 78, 79, 80 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (π§ βΎ πΆ) = π§) |
82 | 17 | reseq2d 5982 |
. . . . . . . . 9
β’ (π β (π§ βΎ πΆ) = (π§ βΎ (π΄ βͺ π΅))) |
83 | 82 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (π§ βΎ πΆ) = (π§ βΎ (π΄ βͺ π΅))) |
84 | 81, 83 | eqtr3d 2775 |
. . . . . . 7
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β π§ = (π§ βΎ (π΄ βͺ π΅))) |
85 | | resundi 5996 |
. . . . . . 7
β’ (π§ βΎ (π΄ βͺ π΅)) = ((π§ βΎ π΄) βͺ (π§ βΎ π΅)) |
86 | 84, 85 | eqtrdi 2789 |
. . . . . 6
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β π§ = ((π§ βΎ π΄) βͺ (π§ βΎ π΅))) |
87 | | uneq12 4159 |
. . . . . . 7
β’
(((1st βπ€) = (π§ βΎ π΄) β§ (2nd βπ€) = (π§ βΎ π΅)) β ((1st βπ€) βͺ (2nd
βπ€)) = ((π§ βΎ π΄) βͺ (π§ βΎ π΅))) |
88 | 87 | eqeq2d 2744 |
. . . . . 6
β’
(((1st βπ€) = (π§ βΎ π΄) β§ (2nd βπ€) = (π§ βΎ π΅)) β (π§ = ((1st βπ€) βͺ (2nd βπ€)) β π§ = ((π§ βΎ π΄) βͺ (π§ βΎ π΅)))) |
89 | 86, 88 | syl5ibrcom 246 |
. . . . 5
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (((1st
βπ€) = (π§ βΎ π΄) β§ (2nd βπ€) = (π§ βΎ π΅)) β π§ = ((1st βπ€) βͺ (2nd βπ€)))) |
90 | | ixpfn 8897 |
. . . . . . . . . . . 12
β’
((1st βπ€) β Xπ β π΄ βͺ (πΉβπ) β (1st βπ€) Fn π΄) |
91 | 29, 90 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π€ β (π Γ π)) β (1st βπ€) Fn π΄) |
92 | 91 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (1st
βπ€) Fn π΄) |
93 | | dffn2 6720 |
. . . . . . . . . 10
β’
((1st βπ€) Fn π΄ β (1st βπ€):π΄βΆV) |
94 | 92, 93 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (1st
βπ€):π΄βΆV) |
95 | 51 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β (π Γ π)) β Xπ β π΅ βͺ (πΉβπ) = π) |
96 | 31, 95 | eleqtrrd 2837 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β (π Γ π)) β (2nd βπ€) β Xπ β
π΅ βͺ (πΉβπ)) |
97 | | ixpfn 8897 |
. . . . . . . . . . . 12
β’
((2nd βπ€) β Xπ β π΅ βͺ (πΉβπ) β (2nd βπ€) Fn π΅) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π€ β (π Γ π)) β (2nd βπ€) Fn π΅) |
99 | 98 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (2nd
βπ€) Fn π΅) |
100 | | dffn2 6720 |
. . . . . . . . . 10
β’
((2nd βπ€) Fn π΅ β (2nd βπ€):π΅βΆV) |
101 | 99, 100 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (2nd
βπ€):π΅βΆV) |
102 | | res0 5986 |
. . . . . . . . . . 11
β’
((1st βπ€) βΎ β
) = β
|
103 | | res0 5986 |
. . . . . . . . . . 11
β’
((2nd βπ€) βΎ β
) = β
|
104 | 102, 103 | eqtr4i 2764 |
. . . . . . . . . 10
β’
((1st βπ€) βΎ β
) = ((2nd
βπ€) βΎ
β
) |
105 | 33 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (π΄ β© π΅) = β
) |
106 | 105 | reseq2d 5982 |
. . . . . . . . . 10
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β ((1st
βπ€) βΎ (π΄ β© π΅)) = ((1st βπ€) βΎ
β
)) |
107 | 105 | reseq2d 5982 |
. . . . . . . . . 10
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β ((2nd
βπ€) βΎ (π΄ β© π΅)) = ((2nd βπ€) βΎ
β
)) |
108 | 104, 106,
107 | 3eqtr4a 2799 |
. . . . . . . . 9
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β ((1st
βπ€) βΎ (π΄ β© π΅)) = ((2nd βπ€) βΎ (π΄ β© π΅))) |
109 | | fresaunres1 6765 |
. . . . . . . . 9
β’
(((1st βπ€):π΄βΆV β§ (2nd βπ€):π΅βΆV β§ ((1st
βπ€) βΎ (π΄ β© π΅)) = ((2nd βπ€) βΎ (π΄ β© π΅))) β (((1st βπ€) βͺ (2nd
βπ€)) βΎ π΄) = (1st βπ€)) |
110 | 94, 101, 108, 109 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (((1st
βπ€) βͺ
(2nd βπ€))
βΎ π΄) =
(1st βπ€)) |
111 | 110 | eqcomd 2739 |
. . . . . . 7
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (1st
βπ€) =
(((1st βπ€)
βͺ (2nd βπ€)) βΎ π΄)) |
112 | | fresaunres2 6764 |
. . . . . . . . 9
β’
(((1st βπ€):π΄βΆV β§ (2nd βπ€):π΅βΆV β§ ((1st
βπ€) βΎ (π΄ β© π΅)) = ((2nd βπ€) βΎ (π΄ β© π΅))) β (((1st βπ€) βͺ (2nd
βπ€)) βΎ π΅) = (2nd βπ€)) |
113 | 94, 101, 108, 112 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (((1st
βπ€) βͺ
(2nd βπ€))
βΎ π΅) =
(2nd βπ€)) |
114 | 113 | eqcomd 2739 |
. . . . . . 7
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (2nd
βπ€) =
(((1st βπ€)
βͺ (2nd βπ€)) βΎ π΅)) |
115 | 111, 114 | jca 513 |
. . . . . 6
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β ((1st
βπ€) =
(((1st βπ€)
βͺ (2nd βπ€)) βΎ π΄) β§ (2nd βπ€) = (((1st
βπ€) βͺ
(2nd βπ€))
βΎ π΅))) |
116 | | reseq1 5976 |
. . . . . . . 8
β’ (π§ = ((1st βπ€) βͺ (2nd
βπ€)) β (π§ βΎ π΄) = (((1st βπ€) βͺ (2nd
βπ€)) βΎ π΄)) |
117 | 116 | eqeq2d 2744 |
. . . . . . 7
β’ (π§ = ((1st βπ€) βͺ (2nd
βπ€)) β
((1st βπ€)
= (π§ βΎ π΄) β (1st
βπ€) =
(((1st βπ€)
βͺ (2nd βπ€)) βΎ π΄))) |
118 | | reseq1 5976 |
. . . . . . . 8
β’ (π§ = ((1st βπ€) βͺ (2nd
βπ€)) β (π§ βΎ π΅) = (((1st βπ€) βͺ (2nd
βπ€)) βΎ π΅)) |
119 | 118 | eqeq2d 2744 |
. . . . . . 7
β’ (π§ = ((1st βπ€) βͺ (2nd
βπ€)) β
((2nd βπ€)
= (π§ βΎ π΅) β (2nd
βπ€) =
(((1st βπ€)
βͺ (2nd βπ€)) βΎ π΅))) |
120 | 117, 119 | anbi12d 632 |
. . . . . 6
β’ (π§ = ((1st βπ€) βͺ (2nd
βπ€)) β
(((1st βπ€)
= (π§ βΎ π΄) β§ (2nd
βπ€) = (π§ βΎ π΅)) β ((1st βπ€) = (((1st
βπ€) βͺ
(2nd βπ€))
βΎ π΄) β§
(2nd βπ€) =
(((1st βπ€)
βͺ (2nd βπ€)) βΎ π΅)))) |
121 | 115, 120 | syl5ibrcom 246 |
. . . . 5
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (π§ = ((1st βπ€) βͺ (2nd βπ€)) β ((1st
βπ€) = (π§ βΎ π΄) β§ (2nd βπ€) = (π§ βΎ π΅)))) |
122 | 89, 121 | impbid 211 |
. . . 4
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (((1st
βπ€) = (π§ βΎ π΄) β§ (2nd βπ€) = (π§ βΎ π΅)) β π§ = ((1st βπ€) βͺ (2nd βπ€)))) |
123 | 77, 122 | bitrd 279 |
. . 3
β’ ((π β§ (π€ β (π Γ π) β§ π§ β βͺ π½)) β (π€ = β¨(π§ βΎ π΄), (π§ βΎ π΅)β© β π§ = ((1st βπ€) βͺ (2nd βπ€)))) |
124 | 8, 62, 75, 123 | f1ocnv2d 7659 |
. 2
β’ (π β (πΊ:(π Γ π)β1-1-ontoββͺ π½
β§ β‘πΊ = (π§ β βͺ π½ β¦ β¨(π§ βΎ π΄), (π§ βΎ π΅)β©))) |
125 | 124 | simprd 497 |
1
β’ (π β β‘πΊ = (π§ β βͺ π½ β¦ β¨(π§ βΎ π΄), (π§ βΎ π΅)β©)) |