Step | Hyp | Ref
| Expression |
1 | | txcmp.s |
. . 3
β’ (π β π β Comp) |
2 | | txcmp.x |
. . . . 5
β’ π = βͺ
π
|
3 | | txcmp.y |
. . . . 5
β’ π = βͺ
π |
4 | | txcmp.r |
. . . . . 6
β’ (π β π
β Comp) |
5 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β π
β Comp) |
6 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β π β Comp) |
7 | | txcmp.w |
. . . . . 6
β’ (π β π β (π
Γt π)) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β π β (π
Γt π)) |
9 | | txcmp.u |
. . . . . 6
β’ (π β (π Γ π) = βͺ π) |
10 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β (π Γ π) = βͺ π) |
11 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β π) β π₯ β π) |
12 | 2, 3, 5, 6, 8, 10,
11 | txcmplem1 22841 |
. . . 4
β’ ((π β§ π₯ β π) β βπ’ β π (π₯ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) |
13 | 12 | ralrimiva 3140 |
. . 3
β’ (π β βπ₯ β π βπ’ β π (π₯ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) |
14 | | unieq 4855 |
. . . . 5
β’ (π£ = (πβπ’) β βͺ π£ = βͺ
(πβπ’)) |
15 | 14 | sseq2d 3958 |
. . . 4
β’ (π£ = (πβπ’) β ((π Γ π’) β βͺ π£ β (π Γ π’) β βͺ (πβπ’))) |
16 | 3, 15 | cmpcovf 22591 |
. . 3
β’ ((π β Comp β§ βπ₯ β π βπ’ β π (π₯ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) β βπ€ β (π« π β© Fin)(π = βͺ π€ β§ βπ(π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) |
17 | 1, 13, 16 | syl2anc 585 |
. 2
β’ (π β βπ€ β (π« π β© Fin)(π = βͺ π€ β§ βπ(π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) |
18 | | simprrl 779 |
. . . . . . . . . . 11
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β π:π€βΆ(π« π β© Fin)) |
19 | | ffn 6630 |
. . . . . . . . . . 11
β’ (π:π€βΆ(π« π β© Fin) β π Fn π€) |
20 | | fniunfv 7152 |
. . . . . . . . . . 11
β’ (π Fn π€ β βͺ
π§ β π€ (πβπ§) = βͺ ran π) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . 10
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βͺ π§ β π€ (πβπ§) = βͺ ran π) |
22 | 18 | frnd 6638 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β ran π β (π« π β© Fin)) |
23 | | inss1 4168 |
. . . . . . . . . . . 12
β’
(π« π β©
Fin) β π« π |
24 | 22, 23 | sstrdi 3938 |
. . . . . . . . . . 11
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β ran π β π« π) |
25 | | sspwuni 5036 |
. . . . . . . . . . 11
β’ (ran
π β π« π β βͺ ran π β π) |
26 | 24, 25 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βͺ ran
π β π) |
27 | 21, 26 | eqsstrd 3964 |
. . . . . . . . 9
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βͺ π§ β π€ (πβπ§) β π) |
28 | | vex 3441 |
. . . . . . . . . . 11
β’ π€ β V |
29 | | fvex 6817 |
. . . . . . . . . . 11
β’ (πβπ§) β V |
30 | 28, 29 | iunex 7843 |
. . . . . . . . . 10
β’ βͺ π§ β π€ (πβπ§) β V |
31 | 30 | elpw 4543 |
. . . . . . . . 9
β’ (βͺ π§ β π€ (πβπ§) β π« π β βͺ
π§ β π€ (πβπ§) β π) |
32 | 27, 31 | sylibr 233 |
. . . . . . . 8
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βͺ π§ β π€ (πβπ§) β π« π) |
33 | | inss2 4169 |
. . . . . . . . . 10
β’
(π« π β©
Fin) β Fin |
34 | | simplr 767 |
. . . . . . . . . 10
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β π€ β (π« π β© Fin)) |
35 | 33, 34 | sselid 3924 |
. . . . . . . . 9
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β π€ β Fin) |
36 | | inss2 4169 |
. . . . . . . . . . 11
β’
(π« π β©
Fin) β Fin |
37 | | fss 6647 |
. . . . . . . . . . 11
β’ ((π:π€βΆ(π« π β© Fin) β§ (π« π β© Fin) β Fin) β
π:π€βΆFin) |
38 | 18, 36, 37 | sylancl 587 |
. . . . . . . . . 10
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β π:π€βΆFin) |
39 | | ffvelcdm 6991 |
. . . . . . . . . . 11
β’ ((π:π€βΆFin β§ π§ β π€) β (πβπ§) β Fin) |
40 | 39 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (π:π€βΆFin β βπ§ β π€ (πβπ§) β Fin) |
41 | 38, 40 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βπ§ β π€ (πβπ§) β Fin) |
42 | | iunfi 9155 |
. . . . . . . . 9
β’ ((π€ β Fin β§ βπ§ β π€ (πβπ§) β Fin) β βͺ π§ β π€ (πβπ§) β Fin) |
43 | 35, 41, 42 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βͺ π§ β π€ (πβπ§) β Fin) |
44 | 32, 43 | elind 4134 |
. . . . . . 7
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βͺ π§ β π€ (πβπ§) β (π« π β© Fin)) |
45 | | simprl 769 |
. . . . . . . . . . . . 13
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β π = βͺ π€) |
46 | | uniiun 4995 |
. . . . . . . . . . . . 13
β’ βͺ π€ =
βͺ π§ β π€ π§ |
47 | 45, 46 | eqtrdi 2792 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β π = βͺ π§ β π€ π§) |
48 | 47 | xpeq2d 5630 |
. . . . . . . . . . 11
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β (π Γ π) = (π Γ βͺ
π§ β π€ π§)) |
49 | | xpiundi 5668 |
. . . . . . . . . . 11
β’ (π Γ βͺ π§ β π€ π§) = βͺ π§ β π€ (π Γ π§) |
50 | 48, 49 | eqtrdi 2792 |
. . . . . . . . . 10
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β (π Γ π) = βͺ
π§ β π€ (π Γ π§)) |
51 | | simprrr 780 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βπ’ β π€ (π Γ π’) β βͺ (πβπ’)) |
52 | | xpeq2 5621 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β (π Γ π’) = (π Γ π§)) |
53 | | fveq2 6804 |
. . . . . . . . . . . . . . 15
β’ (π’ = π§ β (πβπ’) = (πβπ§)) |
54 | 53 | unieqd 4858 |
. . . . . . . . . . . . . 14
β’ (π’ = π§ β βͺ (πβπ’) = βͺ (πβπ§)) |
55 | 52, 54 | sseq12d 3959 |
. . . . . . . . . . . . 13
β’ (π’ = π§ β ((π Γ π’) β βͺ (πβπ’) β (π Γ π§) β βͺ (πβπ§))) |
56 | 55 | cbvralvw 3222 |
. . . . . . . . . . . 12
β’
(βπ’ β
π€ (π Γ π’) β βͺ (πβπ’) β βπ§ β π€ (π Γ π§) β βͺ (πβπ§)) |
57 | 51, 56 | sylib 217 |
. . . . . . . . . . 11
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βπ§ β π€ (π Γ π§) β βͺ (πβπ§)) |
58 | | ss2iun 4949 |
. . . . . . . . . . 11
β’
(βπ§ β
π€ (π Γ π§) β βͺ (πβπ§) β βͺ
π§ β π€ (π Γ π§) β βͺ
π§ β π€ βͺ (πβπ§)) |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βͺ π§ β π€ (π Γ π§) β βͺ
π§ β π€ βͺ (πβπ§)) |
60 | 50, 59 | eqsstrd 3964 |
. . . . . . . . 9
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β (π Γ π) β βͺ π§ β π€ βͺ (πβπ§)) |
61 | 18 | ffvelcdmda 6993 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β§ π§ β π€) β (πβπ§) β (π« π β© Fin)) |
62 | 23, 61 | sselid 3924 |
. . . . . . . . . . . . 13
β’ ((((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β§ π§ β π€) β (πβπ§) β π« π) |
63 | | elpwi 4546 |
. . . . . . . . . . . . 13
β’ ((πβπ§) β π« π β (πβπ§) β π) |
64 | | uniss 4852 |
. . . . . . . . . . . . 13
β’ ((πβπ§) β π β βͺ (πβπ§) β βͺ π) |
65 | 62, 63, 64 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β§ π§ β π€) β βͺ (πβπ§) β βͺ π) |
66 | 9 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β§ π§ β π€) β (π Γ π) = βͺ π) |
67 | 65, 66 | sseqtrrd 3967 |
. . . . . . . . . . 11
β’ ((((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β§ π§ β π€) β βͺ (πβπ§) β (π Γ π)) |
68 | 67 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βπ§ β π€ βͺ (πβπ§) β (π Γ π)) |
69 | | iunss 4982 |
. . . . . . . . . 10
β’ (βͺ π§ β π€ βͺ (πβπ§) β (π Γ π) β βπ§ β π€ βͺ (πβπ§) β (π Γ π)) |
70 | 68, 69 | sylibr 233 |
. . . . . . . . 9
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βͺ π§ β π€ βͺ (πβπ§) β (π Γ π)) |
71 | 60, 70 | eqssd 3943 |
. . . . . . . 8
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β (π Γ π) = βͺ
π§ β π€ βͺ (πβπ§)) |
72 | | iuncom4 4939 |
. . . . . . . 8
β’ βͺ π§ β π€ βͺ (πβπ§) = βͺ βͺ π§ β π€ (πβπ§) |
73 | 71, 72 | eqtrdi 2792 |
. . . . . . 7
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β (π Γ π) = βͺ βͺ π§ β π€ (πβπ§)) |
74 | | unieq 4855 |
. . . . . . . 8
β’ (π£ = βͺ π§ β π€ (πβπ§) β βͺ π£ = βͺ
βͺ π§ β π€ (πβπ§)) |
75 | 74 | rspceeqv 3580 |
. . . . . . 7
β’
((βͺ π§ β π€ (πβπ§) β (π« π β© Fin) β§ (π Γ π) = βͺ βͺ π§ β π€ (πβπ§)) β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£) |
76 | 44, 73, 75 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π€ β (π« π β© Fin)) β§ (π = βͺ π€ β§ (π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)))) β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£) |
77 | 76 | expr 458 |
. . . . 5
β’ (((π β§ π€ β (π« π β© Fin)) β§ π = βͺ π€) β ((π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)) β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£)) |
78 | 77 | exlimdv 1934 |
. . . 4
β’ (((π β§ π€ β (π« π β© Fin)) β§ π = βͺ π€) β (βπ(π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’)) β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£)) |
79 | 78 | expimpd 455 |
. . 3
β’ ((π β§ π€ β (π« π β© Fin)) β ((π = βͺ π€ β§ βπ(π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’))) β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£)) |
80 | 79 | rexlimdva 3149 |
. 2
β’ (π β (βπ€ β (π« π β© Fin)(π = βͺ π€ β§ βπ(π:π€βΆ(π« π β© Fin) β§ βπ’ β π€ (π Γ π’) β βͺ (πβπ’))) β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£)) |
81 | 17, 80 | mpd 15 |
1
β’ (π β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£) |