Step | Hyp | Ref
| Expression |
1 | | txtube.r |
. . 3
β’ (π β π
β Comp) |
2 | | eleq1 2822 |
. . . . . . . 8
β’ (π¦ = β¨π₯, π΄β© β (π¦ β (π’ Γ π£) β β¨π₯, π΄β© β (π’ Γ π£))) |
3 | 2 | anbi1d 631 |
. . . . . . 7
β’ (π¦ = β¨π₯, π΄β© β ((π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π) β (β¨π₯, π΄β© β (π’ Γ π£) β§ (π’ Γ π£) β π))) |
4 | 3 | 2rexbidv 3210 |
. . . . . 6
β’ (π¦ = β¨π₯, π΄β© β (βπ’ β π
βπ£ β π (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π) β βπ’ β π
βπ£ β π (β¨π₯, π΄β© β (π’ Γ π£) β§ (π’ Γ π£) β π))) |
5 | | txtube.w |
. . . . . . . 8
β’ (π β π β (π
Γt π)) |
6 | | txtube.s |
. . . . . . . . 9
β’ (π β π β Top) |
7 | | eltx 22935 |
. . . . . . . . 9
β’ ((π
β Comp β§ π β Top) β (π β (π
Γt π) β βπ¦ β π βπ’ β π
βπ£ β π (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π))) |
8 | 1, 6, 7 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π β (π
Γt π) β βπ¦ β π βπ’ β π
βπ£ β π (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π))) |
9 | 5, 8 | mpbid 231 |
. . . . . . 7
β’ (π β βπ¦ β π βπ’ β π
βπ£ β π (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π)) |
10 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ¦ β π βπ’ β π
βπ£ β π (π¦ β (π’ Γ π£) β§ (π’ Γ π£) β π)) |
11 | | txtube.u |
. . . . . . . 8
β’ (π β (π Γ {π΄}) β π) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π Γ {π΄}) β π) |
13 | | id 22 |
. . . . . . . 8
β’ (π₯ β π β π₯ β π) |
14 | | txtube.a |
. . . . . . . . 9
β’ (π β π΄ β π) |
15 | | snidg 4621 |
. . . . . . . . 9
β’ (π΄ β π β π΄ β {π΄}) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
β’ (π β π΄ β {π΄}) |
17 | | opelxpi 5671 |
. . . . . . . 8
β’ ((π₯ β π β§ π΄ β {π΄}) β β¨π₯, π΄β© β (π Γ {π΄})) |
18 | 13, 16, 17 | syl2anr 598 |
. . . . . . 7
β’ ((π β§ π₯ β π) β β¨π₯, π΄β© β (π Γ {π΄})) |
19 | 12, 18 | sseldd 3946 |
. . . . . 6
β’ ((π β§ π₯ β π) β β¨π₯, π΄β© β π) |
20 | 4, 10, 19 | rspcdva 3581 |
. . . . 5
β’ ((π β§ π₯ β π) β βπ’ β π
βπ£ β π (β¨π₯, π΄β© β (π’ Γ π£) β§ (π’ Γ π£) β π)) |
21 | | opelxp 5670 |
. . . . . . . . . 10
β’
(β¨π₯, π΄β© β (π’ Γ π£) β (π₯ β π’ β§ π΄ β π£)) |
22 | 21 | anbi1i 625 |
. . . . . . . . 9
β’
((β¨π₯, π΄β© β (π’ Γ π£) β§ (π’ Γ π£) β π) β ((π₯ β π’ β§ π΄ β π£) β§ (π’ Γ π£) β π)) |
23 | | anass 470 |
. . . . . . . . 9
β’ (((π₯ β π’ β§ π΄ β π£) β§ (π’ Γ π£) β π) β (π₯ β π’ β§ (π΄ β π£ β§ (π’ Γ π£) β π))) |
24 | 22, 23 | bitri 275 |
. . . . . . . 8
β’
((β¨π₯, π΄β© β (π’ Γ π£) β§ (π’ Γ π£) β π) β (π₯ β π’ β§ (π΄ β π£ β§ (π’ Γ π£) β π))) |
25 | 24 | rexbii 3094 |
. . . . . . 7
β’
(βπ£ β
π (β¨π₯, π΄β© β (π’ Γ π£) β§ (π’ Γ π£) β π) β βπ£ β π (π₯ β π’ β§ (π΄ β π£ β§ (π’ Γ π£) β π))) |
26 | | r19.42v 3184 |
. . . . . . 7
β’
(βπ£ β
π (π₯ β π’ β§ (π΄ β π£ β§ (π’ Γ π£) β π)) β (π₯ β π’ β§ βπ£ β π (π΄ β π£ β§ (π’ Γ π£) β π))) |
27 | 25, 26 | bitri 275 |
. . . . . 6
β’
(βπ£ β
π (β¨π₯, π΄β© β (π’ Γ π£) β§ (π’ Γ π£) β π) β (π₯ β π’ β§ βπ£ β π (π΄ β π£ β§ (π’ Γ π£) β π))) |
28 | 27 | rexbii 3094 |
. . . . 5
β’
(βπ’ β
π
βπ£ β π (β¨π₯, π΄β© β (π’ Γ π£) β§ (π’ Γ π£) β π) β βπ’ β π
(π₯ β π’ β§ βπ£ β π (π΄ β π£ β§ (π’ Γ π£) β π))) |
29 | 20, 28 | sylib 217 |
. . . 4
β’ ((π β§ π₯ β π) β βπ’ β π
(π₯ β π’ β§ βπ£ β π (π΄ β π£ β§ (π’ Γ π£) β π))) |
30 | 29 | ralrimiva 3140 |
. . 3
β’ (π β βπ₯ β π βπ’ β π
(π₯ β π’ β§ βπ£ β π (π΄ β π£ β§ (π’ Γ π£) β π))) |
31 | | txtube.x |
. . . 4
β’ π = βͺ
π
|
32 | | eleq2 2823 |
. . . . 5
β’ (π£ = (πβπ’) β (π΄ β π£ β π΄ β (πβπ’))) |
33 | | xpeq2 5655 |
. . . . . 6
β’ (π£ = (πβπ’) β (π’ Γ π£) = (π’ Γ (πβπ’))) |
34 | 33 | sseq1d 3976 |
. . . . 5
β’ (π£ = (πβπ’) β ((π’ Γ π£) β π β (π’ Γ (πβπ’)) β π)) |
35 | 32, 34 | anbi12d 632 |
. . . 4
β’ (π£ = (πβπ’) β ((π΄ β π£ β§ (π’ Γ π£) β π) β (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π))) |
36 | 31, 35 | cmpcovf 22758 |
. . 3
β’ ((π
β Comp β§ βπ₯ β π βπ’ β π
(π₯ β π’ β§ βπ£ β π (π΄ β π£ β§ (π’ Γ π£) β π))) β βπ‘ β (π« π
β© Fin)(π = βͺ π‘ β§ βπ(π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) |
37 | 1, 30, 36 | syl2anc 585 |
. 2
β’ (π β βπ‘ β (π« π
β© Fin)(π = βͺ π‘ β§ βπ(π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) |
38 | | rint0 4952 |
. . . . . . . . . 10
β’ (ran
π = β
β (π β© β© ran π) = π) |
39 | 38 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π = β
) β (π β© β© ran
π) = π) |
40 | | txtube.y |
. . . . . . . . . . . 12
β’ π = βͺ
π |
41 | 40 | topopn 22271 |
. . . . . . . . . . 11
β’ (π β Top β π β π) |
42 | 6, 41 | syl 17 |
. . . . . . . . . 10
β’ (π β π β π) |
43 | 42 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π = β
) β π β π) |
44 | 39, 43 | eqeltrd 2834 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π = β
) β (π β© β© ran
π) β π) |
45 | 6 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β π β Top) |
46 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π:π‘βΆπ) |
47 | 46 | frnd 6677 |
. . . . . . . . . . . . . 14
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β ran π β π) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β ran π β π) |
49 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β ran π β β
) |
50 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π‘ β (π« π
β© Fin)) |
51 | 50 | elin2d 4160 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π‘ β Fin) |
52 | 46 | ffnd 6670 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π Fn π‘) |
53 | | dffn4 6763 |
. . . . . . . . . . . . . . . 16
β’ (π Fn π‘ β π:π‘βontoβran π) |
54 | 52, 53 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π:π‘βontoβran π) |
55 | | fofi 9285 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β Fin β§ π:π‘βontoβran π) β ran π β Fin) |
56 | 51, 54, 55 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β ran π β Fin) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β ran π β Fin) |
58 | | fiinopn 22266 |
. . . . . . . . . . . . . 14
β’ (π β Top β ((ran π β π β§ ran π β β
β§ ran π β Fin) β β© ran π β π)) |
59 | 58 | imp 408 |
. . . . . . . . . . . . 13
β’ ((π β Top β§ (ran π β π β§ ran π β β
β§ ran π β Fin)) β β© ran π β π) |
60 | 45, 48, 49, 57, 59 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β β© ran π β π) |
61 | | elssuni 4899 |
. . . . . . . . . . . 12
β’ (β© ran π β π β β© ran
π β βͺ π) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β β© ran π β βͺ π) |
63 | 62, 40 | sseqtrrdi 3996 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β β© ran π β π) |
64 | | sseqin2 4176 |
. . . . . . . . . 10
β’ (β© ran π β π β (π β© β© ran
π) = β© ran π) |
65 | 63, 64 | sylib 217 |
. . . . . . . . 9
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β (π β© β© ran
π) = β© ran π) |
66 | 65, 60 | eqeltrd 2834 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β§ ran π β β
) β (π β© β© ran
π) β π) |
67 | 44, 66 | pm2.61dane 3029 |
. . . . . . 7
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β (π β© β© ran
π) β π) |
68 | 14 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π΄ β π) |
69 | | simprrr 781 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)) |
70 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π) β π΄ β (πβπ’)) |
71 | 70 | ralimi 3083 |
. . . . . . . . . . 11
β’
(βπ’ β
π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π) β βπ’ β π‘ π΄ β (πβπ’)) |
72 | 69, 71 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β βπ’ β π‘ π΄ β (πβπ’)) |
73 | | eliin 4960 |
. . . . . . . . . . 11
β’ (π΄ β π β (π΄ β β©
π’ β π‘ (πβπ’) β βπ’ β π‘ π΄ β (πβπ’))) |
74 | 68, 73 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β (π΄ β β©
π’ β π‘ (πβπ’) β βπ’ β π‘ π΄ β (πβπ’))) |
75 | 72, 74 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π΄ β β©
π’ β π‘ (πβπ’)) |
76 | | fniinfv 6920 |
. . . . . . . . . 10
β’ (π Fn π‘ β β©
π’ β π‘ (πβπ’) = β© ran π) |
77 | 52, 76 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β β© π’ β π‘ (πβπ’) = β© ran π) |
78 | 75, 77 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π΄ β β© ran
π) |
79 | 68, 78 | elind 4155 |
. . . . . . 7
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π΄ β (π β© β© ran
π)) |
80 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π = βͺ π‘) |
81 | | uniiun 5019 |
. . . . . . . . . . 11
β’ βͺ π‘ =
βͺ π’ β π‘ π’ |
82 | 80, 81 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β π = βͺ π’ β π‘ π’) |
83 | 82 | xpeq1d 5663 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β (π Γ (π β© β© ran
π)) = (βͺ π’ β π‘ π’ Γ (π β© β© ran
π))) |
84 | | xpiundir 5704 |
. . . . . . . . 9
β’ (βͺ π’ β π‘ π’ Γ (π β© β© ran
π)) = βͺ π’ β π‘ (π’ Γ (π β© β© ran
π)) |
85 | 83, 84 | eqtrdi 2789 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β (π Γ (π β© β© ran
π)) = βͺ π’ β π‘ (π’ Γ (π β© β© ran
π))) |
86 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π) β (π’ Γ (πβπ’)) β π) |
87 | 86 | ralimi 3083 |
. . . . . . . . . . 11
β’
(βπ’ β
π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π) β βπ’ β π‘ (π’ Γ (πβπ’)) β π) |
88 | 69, 87 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β βπ’ β π‘ (π’ Γ (πβπ’)) β π) |
89 | | inss2 4190 |
. . . . . . . . . . . . 13
β’ (π β© β© ran π) β β© ran
π |
90 | 76 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π Fn π‘ β§ π’ β π‘) β β©
π’ β π‘ (πβπ’) = β© ran π) |
91 | | iinss2 5018 |
. . . . . . . . . . . . . . 15
β’ (π’ β π‘ β β©
π’ β π‘ (πβπ’) β (πβπ’)) |
92 | 91 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π Fn π‘ β§ π’ β π‘) β β©
π’ β π‘ (πβπ’) β (πβπ’)) |
93 | 90, 92 | eqsstrrd 3984 |
. . . . . . . . . . . . 13
β’ ((π Fn π‘ β§ π’ β π‘) β β© ran
π β (πβπ’)) |
94 | 89, 93 | sstrid 3956 |
. . . . . . . . . . . 12
β’ ((π Fn π‘ β§ π’ β π‘) β (π β© β© ran
π) β (πβπ’)) |
95 | | xpss2 5654 |
. . . . . . . . . . . 12
β’ ((π β© β© ran π) β (πβπ’) β (π’ Γ (π β© β© ran
π)) β (π’ Γ (πβπ’))) |
96 | | sstr2 3952 |
. . . . . . . . . . . 12
β’ ((π’ Γ (π β© β© ran
π)) β (π’ Γ (πβπ’)) β ((π’ Γ (πβπ’)) β π β (π’ Γ (π β© β© ran
π)) β π)) |
97 | 94, 95, 96 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π Fn π‘ β§ π’ β π‘) β ((π’ Γ (πβπ’)) β π β (π’ Γ (π β© β© ran
π)) β π)) |
98 | 97 | ralimdva 3161 |
. . . . . . . . . 10
β’ (π Fn π‘ β (βπ’ β π‘ (π’ Γ (πβπ’)) β π β βπ’ β π‘ (π’ Γ (π β© β© ran
π)) β π)) |
99 | 52, 88, 98 | sylc 65 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β βπ’ β π‘ (π’ Γ (π β© β© ran
π)) β π) |
100 | | iunss 5006 |
. . . . . . . . 9
β’ (βͺ π’ β π‘ (π’ Γ (π β© β© ran
π)) β π β βπ’ β π‘ (π’ Γ (π β© β© ran
π)) β π) |
101 | 99, 100 | sylibr 233 |
. . . . . . . 8
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β βͺ π’ β π‘ (π’ Γ (π β© β© ran
π)) β π) |
102 | 85, 101 | eqsstrd 3983 |
. . . . . . 7
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β (π Γ (π β© β© ran
π)) β π) |
103 | | eleq2 2823 |
. . . . . . . . 9
β’ (π’ = (π β© β© ran
π) β (π΄ β π’ β π΄ β (π β© β© ran
π))) |
104 | | xpeq2 5655 |
. . . . . . . . . 10
β’ (π’ = (π β© β© ran
π) β (π Γ π’) = (π Γ (π β© β© ran
π))) |
105 | 104 | sseq1d 3976 |
. . . . . . . . 9
β’ (π’ = (π β© β© ran
π) β ((π Γ π’) β π β (π Γ (π β© β© ran
π)) β π)) |
106 | 103, 105 | anbi12d 632 |
. . . . . . . 8
β’ (π’ = (π β© β© ran
π) β ((π΄ β π’ β§ (π Γ π’) β π) β (π΄ β (π β© β© ran
π) β§ (π Γ (π β© β© ran
π)) β π))) |
107 | 106 | rspcev 3580 |
. . . . . . 7
β’ (((π β© β© ran π) β π β§ (π΄ β (π β© β© ran
π) β§ (π Γ (π β© β© ran
π)) β π)) β βπ’ β π (π΄ β π’ β§ (π Γ π’) β π)) |
108 | 67, 79, 102, 107 | syl12anc 836 |
. . . . . 6
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ (π = βͺ π‘ β§ (π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)))) β βπ’ β π (π΄ β π’ β§ (π Γ π’) β π)) |
109 | 108 | expr 458 |
. . . . 5
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ π = βͺ π‘) β ((π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)) β βπ’ β π (π΄ β π’ β§ (π Γ π’) β π))) |
110 | 109 | exlimdv 1937 |
. . . 4
β’ (((π β§ π‘ β (π« π
β© Fin)) β§ π = βͺ π‘) β (βπ(π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π)) β βπ’ β π (π΄ β π’ β§ (π Γ π’) β π))) |
111 | 110 | expimpd 455 |
. . 3
β’ ((π β§ π‘ β (π« π
β© Fin)) β ((π = βͺ π‘ β§ βπ(π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π))) β βπ’ β π (π΄ β π’ β§ (π Γ π’) β π))) |
112 | 111 | rexlimdva 3149 |
. 2
β’ (π β (βπ‘ β (π« π
β© Fin)(π = βͺ π‘ β§ βπ(π:π‘βΆπ β§ βπ’ β π‘ (π΄ β (πβπ’) β§ (π’ Γ (πβπ’)) β π))) β βπ’ β π (π΄ β π’ β§ (π Γ π’) β π))) |
113 | 37, 112 | mpd 15 |
1
β’ (π β βπ’ β π (π΄ β π’ β§ (π Γ π’) β π)) |