Step | Hyp | Ref
| Expression |
1 | | txcmp.r |
. . 3
β’ (π β π
β Comp) |
2 | | id 22 |
. . . . . . . . 9
β’ (π₯ β π β π₯ β π) |
3 | | txcmp.a |
. . . . . . . . 9
β’ (π β π΄ β π) |
4 | | opelxpi 5671 |
. . . . . . . . 9
β’ ((π₯ β π β§ π΄ β π) β β¨π₯, π΄β© β (π Γ π)) |
5 | 2, 3, 4 | syl2anr 598 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β β¨π₯, π΄β© β (π Γ π)) |
6 | | txcmp.u |
. . . . . . . . 9
β’ (π β (π Γ π) = βͺ π) |
7 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (π Γ π) = βͺ π) |
8 | 5, 7 | eleqtrd 2836 |
. . . . . . 7
β’ ((π β§ π₯ β π) β β¨π₯, π΄β© β βͺ
π) |
9 | | eluni2 4870 |
. . . . . . 7
β’
(β¨π₯, π΄β© β βͺ π
β βπ β
π β¨π₯, π΄β© β π) |
10 | 8, 9 | sylib 217 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ β π β¨π₯, π΄β© β π) |
11 | | txcmp.w |
. . . . . . . . . . . 12
β’ (π β π β (π
Γt π)) |
12 | 11 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β π β (π
Γt π)) |
13 | 12 | sselda 3945 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β π) β π β (π
Γt π)) |
14 | | txcmp.s |
. . . . . . . . . . . . 13
β’ (π β π β Comp) |
15 | | eltx 22935 |
. . . . . . . . . . . . 13
β’ ((π
β Comp β§ π β Comp) β (π β (π
Γt π) β βπ¦ β π βπ β π
βπ β π (π¦ β (π Γ π ) β§ (π Γ π ) β π))) |
16 | 1, 14, 15 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π β (π
Γt π) β βπ¦ β π βπ β π
βπ β π (π¦ β (π Γ π ) β§ (π Γ π ) β π))) |
17 | 16 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β (π β (π
Γt π) β βπ¦ β π βπ β π
βπ β π (π¦ β (π Γ π ) β§ (π Γ π ) β π))) |
18 | 17 | biimpa 478 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β (π
Γt π)) β βπ¦ β π βπ β π
βπ β π (π¦ β (π Γ π ) β§ (π Γ π ) β π)) |
19 | 13, 18 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β π) β βπ¦ β π βπ β π
βπ β π (π¦ β (π Γ π ) β§ (π Γ π ) β π)) |
20 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π¦ = β¨π₯, π΄β© β (π¦ β (π Γ π ) β β¨π₯, π΄β© β (π Γ π ))) |
21 | 20 | anbi1d 631 |
. . . . . . . . . . 11
β’ (π¦ = β¨π₯, π΄β© β ((π¦ β (π Γ π ) β§ (π Γ π ) β π) β (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π))) |
22 | 21 | 2rexbidv 3210 |
. . . . . . . . . 10
β’ (π¦ = β¨π₯, π΄β© β (βπ β π
βπ β π (π¦ β (π Γ π ) β§ (π Γ π ) β π) β βπ β π
βπ β π (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π))) |
23 | 22 | rspccv 3577 |
. . . . . . . . 9
β’
(βπ¦ β
π βπ β π
βπ β π (π¦ β (π Γ π ) β§ (π Γ π ) β π) β (β¨π₯, π΄β© β π β βπ β π
βπ β π (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π))) |
24 | 19, 23 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β π) β (β¨π₯, π΄β© β π β βπ β π
βπ β π (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π))) |
25 | | opelxp1 5675 |
. . . . . . . . . . . . 13
β’
(β¨π₯, π΄β© β (π Γ π ) β π₯ β π) |
26 | 25 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ π β π) β§ (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π)) β π₯ β π) |
27 | | opelxp2 5676 |
. . . . . . . . . . . . . . . 16
β’
(β¨π₯, π΄β© β (π Γ π ) β π΄ β π ) |
28 | 27 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ π β π) β§ (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π)) β π΄ β π ) |
29 | 28 | snssd 4770 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ π β π) β§ (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π)) β {π΄} β π ) |
30 | | xpss2 5654 |
. . . . . . . . . . . . . 14
β’ ({π΄} β π β (π Γ {π΄}) β (π Γ π )) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ π β π) β§ (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π)) β (π Γ {π΄}) β (π Γ π )) |
32 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ π β π) β§ (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π)) β (π Γ π ) β π) |
33 | 31, 32 | sstrd 3955 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ π β π) β§ (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π)) β (π Γ {π΄}) β π) |
34 | 26, 33 | jca 513 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π β π) β§ (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π)) β (π₯ β π β§ (π Γ {π΄}) β π)) |
35 | 34 | ex 414 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β π) β ((β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π) β (π₯ β π β§ (π Γ {π΄}) β π))) |
36 | 35 | rexlimdvw 3154 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β π) β (βπ β π (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π) β (π₯ β π β§ (π Γ {π΄}) β π))) |
37 | 36 | reximdv 3164 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β π) β (βπ β π
βπ β π (β¨π₯, π΄β© β (π Γ π ) β§ (π Γ π ) β π) β βπ β π
(π₯ β π β§ (π Γ {π΄}) β π))) |
38 | 24, 37 | syld 47 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β π) β (β¨π₯, π΄β© β π β βπ β π
(π₯ β π β§ (π Γ {π΄}) β π))) |
39 | 38 | reximdva 3162 |
. . . . . 6
β’ ((π β§ π₯ β π) β (βπ β π β¨π₯, π΄β© β π β βπ β π βπ β π
(π₯ β π β§ (π Γ {π΄}) β π))) |
40 | 10, 39 | mpd 15 |
. . . . 5
β’ ((π β§ π₯ β π) β βπ β π βπ β π
(π₯ β π β§ (π Γ {π΄}) β π)) |
41 | | rexcom 3272 |
. . . . . 6
β’
(βπ β
π βπ β π
(π₯ β π β§ (π Γ {π΄}) β π) β βπ β π
βπ β π (π₯ β π β§ (π Γ {π΄}) β π)) |
42 | | r19.42v 3184 |
. . . . . . 7
β’
(βπ β
π (π₯ β π β§ (π Γ {π΄}) β π) β (π₯ β π β§ βπ β π (π Γ {π΄}) β π)) |
43 | 42 | rexbii 3094 |
. . . . . 6
β’
(βπ β
π
βπ β π (π₯ β π β§ (π Γ {π΄}) β π) β βπ β π
(π₯ β π β§ βπ β π (π Γ {π΄}) β π)) |
44 | 41, 43 | bitri 275 |
. . . . 5
β’
(βπ β
π βπ β π
(π₯ β π β§ (π Γ {π΄}) β π) β βπ β π
(π₯ β π β§ βπ β π (π Γ {π΄}) β π)) |
45 | 40, 44 | sylib 217 |
. . . 4
β’ ((π β§ π₯ β π) β βπ β π
(π₯ β π β§ βπ β π (π Γ {π΄}) β π)) |
46 | 45 | ralrimiva 3140 |
. . 3
β’ (π β βπ₯ β π βπ β π
(π₯ β π β§ βπ β π (π Γ {π΄}) β π)) |
47 | | txcmp.x |
. . . 4
β’ π = βͺ
π
|
48 | | sseq2 3971 |
. . . 4
β’ (π = (πβπ) β ((π Γ {π΄}) β π β (π Γ {π΄}) β (πβπ))) |
49 | 47, 48 | cmpcovf 22758 |
. . 3
β’ ((π
β Comp β§ βπ₯ β π βπ β π
(π₯ β π β§ βπ β π (π Γ {π΄}) β π)) β βπ‘ β (π« π
β© Fin)(π = βͺ π‘ β§ βπ(π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) |
50 | 1, 46, 49 | syl2anc 585 |
. 2
β’ (π β βπ‘ β (π« π
β© Fin)(π = βͺ π‘ β§ βπ(π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) |
51 | | txcmp.y |
. . . . . . . 8
β’ π = βͺ
π |
52 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π
β Comp) |
53 | | cmptop 22762 |
. . . . . . . . . 10
β’ (π β Comp β π β Top) |
54 | 14, 53 | syl 17 |
. . . . . . . . 9
β’ (π β π β Top) |
55 | 54 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π β Top) |
56 | | cmptop 22762 |
. . . . . . . . . . 11
β’ (π
β Comp β π
β Top) |
57 | 52, 56 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π
β Top) |
58 | | txtop 22936 |
. . . . . . . . . 10
β’ ((π
β Top β§ π β Top) β (π
Γt π) β Top) |
59 | 57, 55, 58 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β (π
Γt π) β Top) |
60 | | simprrl 780 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π:π‘βΆπ) |
61 | 60 | frnd 6677 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β ran π β π) |
62 | 11 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π β (π
Γt π)) |
63 | 61, 62 | sstrd 3955 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β ran π β (π
Γt π)) |
64 | | uniopn 22262 |
. . . . . . . . 9
β’ (((π
Γt π) β Top β§ ran π β (π
Γt π)) β βͺ ran
π β (π
Γt π)) |
65 | 59, 63, 64 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β βͺ ran
π β (π
Γt π)) |
66 | | simprrr 781 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β βπ β π‘ (π Γ {π΄}) β (πβπ)) |
67 | | ss2iun 4973 |
. . . . . . . . . 10
β’
(βπ β
π‘ (π Γ {π΄}) β (πβπ) β βͺ
π β π‘ (π Γ {π΄}) β βͺ π β π‘ (πβπ)) |
68 | 66, 67 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β βͺ π β π‘ (π Γ {π΄}) β βͺ π β π‘ (πβπ)) |
69 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π = βͺ π‘) |
70 | | uniiun 5019 |
. . . . . . . . . . . 12
β’ βͺ π‘ =
βͺ π β π‘ π |
71 | 69, 70 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π = βͺ π β π‘ π) |
72 | 71 | xpeq1d 5663 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β (π Γ {π΄}) = (βͺ
π β π‘ π Γ {π΄})) |
73 | | xpiundir 5704 |
. . . . . . . . . 10
β’ (βͺ π β π‘ π Γ {π΄}) = βͺ
π β π‘ (π Γ {π΄}) |
74 | 72, 73 | eqtr2di 2790 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β βͺ π β π‘ (π Γ {π΄}) = (π Γ {π΄})) |
75 | 60 | ffnd 6670 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π Fn π‘) |
76 | | fniunfv 7195 |
. . . . . . . . . 10
β’ (π Fn π‘ β βͺ
π β π‘ (πβπ) = βͺ ran π) |
77 | 75, 76 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β βͺ π β π‘ (πβπ) = βͺ ran π) |
78 | 68, 74, 77 | 3sstr3d 3991 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β (π Γ {π΄}) β βͺ ran
π) |
79 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π΄ β π) |
80 | 47, 51, 52, 55, 65, 78, 79 | txtube 23007 |
. . . . . . 7
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β βπ’ β π (π΄ β π’ β§ (π Γ π’) β βͺ ran
π)) |
81 | | vex 3448 |
. . . . . . . . . . . . . 14
β’ π β V |
82 | 81 | rnex 7850 |
. . . . . . . . . . . . 13
β’ ran π β V |
83 | 82 | elpw 4565 |
. . . . . . . . . . . 12
β’ (ran
π β π« π β ran π β π) |
84 | 61, 83 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β ran π β π« π) |
85 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π‘ β (π« π
β© Fin)) |
86 | 85 | elin2d 4160 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π‘ β Fin) |
87 | | dffn4 6763 |
. . . . . . . . . . . . 13
β’ (π Fn π‘ β π:π‘βontoβran π) |
88 | 75, 87 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β π:π‘βontoβran π) |
89 | | fofi 9285 |
. . . . . . . . . . . 12
β’ ((π‘ β Fin β§ π:π‘βontoβran π) β ran π β Fin) |
90 | 86, 88, 89 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β ran π β Fin) |
91 | 84, 90 | elind 4155 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β ran π β (π« π β© Fin)) |
92 | | unieq 4877 |
. . . . . . . . . . . . 13
β’ (π£ = ran π β βͺ π£ = βͺ
ran π) |
93 | 92 | sseq2d 3977 |
. . . . . . . . . . . 12
β’ (π£ = ran π β ((π Γ π’) β βͺ π£ β (π Γ π’) β βͺ ran
π)) |
94 | 93 | rspcev 3580 |
. . . . . . . . . . 11
β’ ((ran
π β (π« π β© Fin) β§ (π Γ π’) β βͺ ran
π) β βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£) |
95 | 94 | ex 414 |
. . . . . . . . . 10
β’ (ran
π β (π« π β© Fin) β ((π Γ π’) β βͺ ran
π β βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) |
96 | 91, 95 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β ((π Γ π’) β βͺ ran
π β βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) |
97 | 96 | anim2d 613 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β ((π΄ β π’ β§ (π Γ π’) β βͺ ran
π) β (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£))) |
98 | 97 | reximdv 3164 |
. . . . . . 7
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β (βπ’ β π (π΄ β π’ β§ (π Γ π’) β βͺ ran
π) β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£))) |
99 | 80, 98 | mpd 15 |
. . . . . 6
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)))) β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) |
100 | 99 | expr 458 |
. . . . 5
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ π = βͺ π‘) β ((π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)) β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£))) |
101 | 100 | exlimdv 1937 |
. . . 4
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ π = βͺ π‘) β (βπ(π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ)) β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£))) |
102 | 101 | expimpd 455 |
. . 3
β’ ((π β§ π‘ β (π« π
β© Fin)) β ((π = βͺ π‘ β§ βπ(π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ))) β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£))) |
103 | 102 | rexlimdva 3149 |
. 2
β’ (π β (βπ‘ β (π« π
β© Fin)(π = βͺ π‘ β§ βπ(π:π‘βΆπ β§ βπ β π‘ (π Γ {π΄}) β (πβπ))) β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£))) |
104 | 50, 103 | mpd 15 |
1
β’ (π β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) |