Step | Hyp | Ref
| Expression |
1 | | dynkin.p |
. . . 4
β’ π = {π β π« π« π β£ (fiβπ ) β π } |
2 | 1 | sigapisys 32811 |
. . 3
β’
(sigAlgebraβπ)
β π |
3 | | dynkin.l |
. . . 4
β’ πΏ = {π β π« π« π β£ (β
β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} |
4 | 3 | sigaldsys 32815 |
. . 3
β’
(sigAlgebraβπ)
β πΏ |
5 | 2, 4 | ssini 4192 |
. 2
β’
(sigAlgebraβπ)
β (π β© πΏ) |
6 | | id 22 |
. . . . . . . . 9
β’ (π‘ β (π β© πΏ) β π‘ β (π β© πΏ)) |
7 | 6 | elin1d 4159 |
. . . . . . . 8
β’ (π‘ β (π β© πΏ) β π‘ β π) |
8 | 1 | ispisys 32808 |
. . . . . . . 8
β’ (π‘ β π β (π‘ β π« π« π β§ (fiβπ‘) β π‘)) |
9 | 7, 8 | sylib 217 |
. . . . . . 7
β’ (π‘ β (π β© πΏ) β (π‘ β π« π« π β§ (fiβπ‘) β π‘)) |
10 | 9 | simpld 496 |
. . . . . 6
β’ (π‘ β (π β© πΏ) β π‘ β π« π« π) |
11 | 10 | elpwid 4570 |
. . . . 5
β’ (π‘ β (π β© πΏ) β π‘ β π« π) |
12 | | dif0 4333 |
. . . . . . 7
β’ (π β β
) = π |
13 | 6 | elin2d 4160 |
. . . . . . . . . . 11
β’ (π‘ β (π β© πΏ) β π‘ β πΏ) |
14 | 3 | isldsys 32812 |
. . . . . . . . . . 11
β’ (π‘ β πΏ β (π‘ β π« π« π β§ (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)))) |
15 | 13, 14 | sylib 217 |
. . . . . . . . . 10
β’ (π‘ β (π β© πΏ) β (π‘ β π« π« π β§ (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)))) |
16 | 15 | simprd 497 |
. . . . . . . . 9
β’ (π‘ β (π β© πΏ) β (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘))) |
17 | 16 | simp2d 1144 |
. . . . . . . 8
β’ (π‘ β (π β© πΏ) β βπ₯ β π‘ (π β π₯) β π‘) |
18 | 16 | simp1d 1143 |
. . . . . . . . 9
β’ (π‘ β (π β© πΏ) β β
β π‘) |
19 | | difeq2 4077 |
. . . . . . . . . . 11
β’ (π₯ = β
β (π β π₯) = (π β β
)) |
20 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (π₯ = β
β π‘ = π‘) |
21 | 19, 20 | eleq12d 2828 |
. . . . . . . . . 10
β’ (π₯ = β
β ((π β π₯) β π‘ β (π β β
) β π‘)) |
22 | 21 | rspcv 3576 |
. . . . . . . . 9
β’ (β
β π‘ β
(βπ₯ β π‘ (π β π₯) β π‘ β (π β β
) β π‘)) |
23 | 18, 22 | syl 17 |
. . . . . . . 8
β’ (π‘ β (π β© πΏ) β (βπ₯ β π‘ (π β π₯) β π‘ β (π β β
) β π‘)) |
24 | 17, 23 | mpd 15 |
. . . . . . 7
β’ (π‘ β (π β© πΏ) β (π β β
) β π‘) |
25 | 12, 24 | eqeltrrid 2839 |
. . . . . 6
β’ (π‘ β (π β© πΏ) β π β π‘) |
26 | | unieq 4877 |
. . . . . . . . . . . 12
β’ (π₯ = β
β βͺ π₯ =
βͺ β
) |
27 | | uni0 4897 |
. . . . . . . . . . . 12
β’ βͺ β
= β
|
28 | 26, 27 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π₯ = β
β βͺ π₯ =
β
) |
29 | 28 | adantl 483 |
. . . . . . . . . 10
β’ ((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ = β
) β βͺ π₯ =
β
) |
30 | 18 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ = β
) β β
β π‘) |
31 | 29, 30 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ = β
) β βͺ π₯
β π‘) |
32 | | vex 3448 |
. . . . . . . . . . . . . 14
β’ π₯ β V |
33 | 32 | 0sdom 9054 |
. . . . . . . . . . . . 13
β’ (β
βΊ π₯ β π₯ β β
) |
34 | 33 | biimpri 227 |
. . . . . . . . . . . 12
β’ (π₯ β β
β β
βΊ π₯) |
35 | 34 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β β
βΊ π₯) |
36 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β π₯ βΌ Ο) |
37 | | nnenom 13891 |
. . . . . . . . . . . . 13
β’ β
β Ο |
38 | 37 | ensymi 8947 |
. . . . . . . . . . . 12
β’ Ο
β β |
39 | | domentr 8956 |
. . . . . . . . . . . 12
β’ ((π₯ βΌ Ο β§ Ο
β β) β π₯
βΌ β) |
40 | 36, 38, 39 | sylancl 587 |
. . . . . . . . . . 11
β’ ((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β π₯ βΌ β) |
41 | | fodomr 9075 |
. . . . . . . . . . 11
β’ ((β
βΊ π₯ β§ π₯ βΌ β) β
βπ π:ββontoβπ₯) |
42 | 35, 40, 41 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β βπ π:ββontoβπ₯) |
43 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
44 | 43 | iundisj 24928 |
. . . . . . . . . . . . 13
β’ βͺ π β β (πβπ) = βͺ π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)) |
45 | | fofn 6759 |
. . . . . . . . . . . . . . 15
β’ (π:ββontoβπ₯ β π Fn β) |
46 | | fniunfv 7195 |
. . . . . . . . . . . . . . 15
β’ (π Fn β β βͺ π β β (πβπ) = βͺ ran π) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π:ββontoβπ₯ β βͺ
π β β (πβπ) = βͺ ran π) |
48 | | forn 6760 |
. . . . . . . . . . . . . . 15
β’ (π:ββontoβπ₯ β ran π = π₯) |
49 | 48 | unieqd 4880 |
. . . . . . . . . . . . . 14
β’ (π:ββontoβπ₯ β βͺ ran
π = βͺ π₯) |
50 | 47, 49 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π:ββontoβπ₯ β βͺ
π β β (πβπ) = βͺ π₯) |
51 | 44, 50 | eqtr3id 2787 |
. . . . . . . . . . . 12
β’ (π:ββontoβπ₯ β βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)) = βͺ π₯) |
52 | 51 | adantl 483 |
. . . . . . . . . . 11
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)) = βͺ π₯) |
53 | | fvex 6856 |
. . . . . . . . . . . . . 14
β’ (πβπ) β V |
54 | | difexg 5285 |
. . . . . . . . . . . . . 14
β’ ((πβπ) β V β ((πβπ) β βͺ
π β (1..^π)(πβπ)) β V) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ ((πβπ) β βͺ
π β (1..^π)(πβπ)) β V |
56 | 55 | dfiun3 5922 |
. . . . . . . . . . . 12
β’ βͺ π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)) = βͺ ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
57 | | nfv 1918 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) |
58 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²ππ¦ |
59 | | nfmpt1 5214 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
60 | 59 | nfrn 5908 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) |
61 | 58, 60 | nfel 2918 |
. . . . . . . . . . . . . . . . . 18
β’
β²π π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
62 | 57, 61 | nfan 1903 |
. . . . . . . . . . . . . . . . 17
β’
β²π(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) |
63 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
64 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) |
65 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²ππ¦ |
66 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²πβ |
67 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π(πβπ) |
68 | | nfiu1 4989 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²πβͺ π β (1..^π)(πβπ) |
69 | 67, 68 | nfdif 4086 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π((πβπ) β βͺ
π β (1..^π)(πβπ)) |
70 | 66, 69 | nfmpt 5213 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
71 | 70 | nfrn 5908 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²πran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) |
72 | 65, 71 | nfel 2918 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
73 | 64, 72 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) |
74 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π π β β |
75 | 73, 74 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) |
76 | 65, 69 | nfeq 2917 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ)) |
77 | 75, 76 | nfan 1903 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(((((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
78 | 6 | ad7antr 737 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π‘ β (π β© πΏ)) |
79 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β π₯ β π« π‘) |
80 | 79 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π₯ β π« π‘) |
81 | 80 | elpwid 4570 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π₯ β π‘) |
82 | | fof 6757 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:ββontoβπ₯ β π:ββΆπ₯) |
83 | 82 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π:ββΆπ₯) |
84 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π β β) |
85 | 83, 84 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β (πβπ) β π₯) |
86 | 81, 85 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β (πβπ) β π‘) |
87 | | fzofi 13885 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1..^π) β
Fin |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β (1..^π) β Fin) |
89 | 81 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β§ π β (1..^π)) β π₯ β π‘) |
90 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β§ π β (1..^π)) β π:ββΆπ₯) |
91 | | fzossnn 13627 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(1..^π) β
β |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β (1..^π) β β) |
93 | 92 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β§ π β (1..^π)) β π β β) |
94 | 90, 93 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β§ π β (1..^π)) β (πβπ) β π₯) |
95 | 89, 94 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β§ π β (1..^π)) β (πβπ) β π‘) |
96 | 1, 3, 77, 78, 86, 88, 95 | sigapildsyslem 32817 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β ((πβπ) β βͺ
π β (1..^π)(πβπ)) β π‘) |
97 | 63, 96 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β§ π β β) β§ π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π¦ β π‘) |
98 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) |
99 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) = (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
100 | 99, 55 | elrnmpti 5916 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β βπ β β π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
101 | 98, 100 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’
((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β βπ β β π¦ = ((πβπ) β βͺ
π β (1..^π)(πβπ))) |
102 | 62, 97, 101 | r19.29af 3250 |
. . . . . . . . . . . . . . . 16
β’
((((((π‘ β
(π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β§ π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))) β π¦ β π‘) |
103 | 102 | ex 414 |
. . . . . . . . . . . . . . 15
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β (π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π¦ β π‘)) |
104 | 103 | ssrdv 3951 |
. . . . . . . . . . . . . 14
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π‘) |
105 | | nnex 12164 |
. . . . . . . . . . . . . . . . 17
β’ β
β V |
106 | 105 | mptex 7174 |
. . . . . . . . . . . . . . . 16
β’ (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β V |
107 | 106 | rnex 7850 |
. . . . . . . . . . . . . . 15
β’ ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β V |
108 | | elpwg 4564 |
. . . . . . . . . . . . . . 15
β’ (ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β V β (ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π« π‘ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π‘)) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π« π‘ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π‘) |
110 | 104, 109 | sylibr 233 |
. . . . . . . . . . . . 13
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β π« π‘) |
111 | 16 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ (π‘ β (π β© πΏ) β βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) |
112 | 111 | ad4antr 731 |
. . . . . . . . . . . . 13
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) |
113 | | nnct 13892 |
. . . . . . . . . . . . . . 15
β’ β
βΌ Ο |
114 | | mptct 10479 |
. . . . . . . . . . . . . . 15
β’ (β
βΌ Ο β (π
β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο) |
115 | 113, 114 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο |
116 | | rnct 10466 |
. . . . . . . . . . . . . 14
β’ ((π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο) |
117 | 115, 116 | mp1i 13 |
. . . . . . . . . . . . 13
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο) |
118 | 43 | iundisj2 24929 |
. . . . . . . . . . . . . 14
β’
Disj π β
β ((πβπ) β βͺ π β (1..^π)(πβπ)) |
119 | | disjrnmpt 31549 |
. . . . . . . . . . . . . 14
β’
(Disj π
β β ((πβπ) β βͺ
π β (1..^π)(πβπ)) β Disj π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))π¦) |
120 | 118, 119 | mp1i 13 |
. . . . . . . . . . . . 13
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β Disj π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))π¦) |
121 | | breq1 5109 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β (π₯ βΌ Ο β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο)) |
122 | | disjeq1 5078 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β (Disj π¦ β π₯ π¦ β Disj π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))π¦)) |
123 | 121, 122 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β (ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο β§ Disj π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))π¦))) |
124 | | unieq 4877 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β βͺ π₯ = βͺ
ran (π β β
β¦ ((πβπ) β βͺ π β (1..^π)(πβπ)))) |
125 | 124 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β (βͺ
π₯ β π‘ β βͺ ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π‘)) |
126 | 123, 125 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) β (((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘) β ((ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο β§ Disj π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))π¦) β βͺ ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π‘))) |
127 | 126 | rspcv 3576 |
. . . . . . . . . . . . . . 15
β’ (ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π« π‘ β (βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘) β ((ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο β§ Disj π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))π¦) β βͺ ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π‘))) |
128 | 127 | imp 408 |
. . . . . . . . . . . . . 14
β’ ((ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π« π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) β ((ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο β§ Disj π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))π¦) β βͺ ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π‘)) |
129 | 128 | imp 408 |
. . . . . . . . . . . . 13
β’ (((ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π« π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) β§ (ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ))) βΌ Ο β§ Disj π¦ β ran (π β β β¦ ((πβπ) β βͺ
π β (1..^π)(πβπ)))π¦)) β βͺ ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π‘) |
130 | 110, 112,
117, 120, 129 | syl22anc 838 |
. . . . . . . . . . . 12
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β βͺ ran
(π β β β¦
((πβπ) β βͺ π β (1..^π)(πβπ))) β π‘) |
131 | 56, 130 | eqeltrid 2838 |
. . . . . . . . . . 11
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β βͺ
π β β ((πβπ) β βͺ
π β (1..^π)(πβπ)) β π‘) |
132 | 52, 131 | eqeltrrd 2835 |
. . . . . . . . . 10
β’
(((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β§ π:ββontoβπ₯) β βͺ π₯ β π‘) |
133 | 42, 132 | exlimddv 1939 |
. . . . . . . . 9
β’ ((((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β§ π₯ β β
) β βͺ π₯
β π‘) |
134 | 31, 133 | pm2.61dane 3029 |
. . . . . . . 8
β’ (((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β§ π₯ βΌ Ο) β βͺ π₯
β π‘) |
135 | 134 | ex 414 |
. . . . . . 7
β’ ((π‘ β (π β© πΏ) β§ π₯ β π« π‘) β (π₯ βΌ Ο β βͺ π₯
β π‘)) |
136 | 135 | ralrimiva 3140 |
. . . . . 6
β’ (π‘ β (π β© πΏ) β βπ₯ β π« π‘(π₯ βΌ Ο β βͺ π₯
β π‘)) |
137 | 25, 17, 136 | 3jca 1129 |
. . . . 5
β’ (π‘ β (π β© πΏ) β (π β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘(π₯ βΌ Ο β βͺ π₯
β π‘))) |
138 | 11, 137 | jca 513 |
. . . 4
β’ (π‘ β (π β© πΏ) β (π‘ β π« π β§ (π β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘(π₯ βΌ Ο β βͺ π₯
β π‘)))) |
139 | | vex 3448 |
. . . . 5
β’ π‘ β V |
140 | | issiga 32768 |
. . . . 5
β’ (π‘ β V β (π‘ β (sigAlgebraβπ) β (π‘ β π« π β§ (π β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘(π₯ βΌ Ο β βͺ π₯
β π‘))))) |
141 | 139, 140 | ax-mp 5 |
. . . 4
β’ (π‘ β (sigAlgebraβπ) β (π‘ β π« π β§ (π β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘(π₯ βΌ Ο β βͺ π₯
β π‘)))) |
142 | 138, 141 | sylibr 233 |
. . 3
β’ (π‘ β (π β© πΏ) β π‘ β (sigAlgebraβπ)) |
143 | 142 | ssriv 3949 |
. 2
β’ (π β© πΏ) β (sigAlgebraβπ) |
144 | 5, 143 | eqssi 3961 |
1
β’
(sigAlgebraβπ)
= (π β© πΏ) |