Step | Hyp | Ref
| Expression |
1 | | ldsysgenld.1 |
. . . . 5
β’ (π β π β π) |
2 | | pwsiga 32793 |
. . . . 5
β’ (π β π β π« π β (sigAlgebraβπ)) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π« π β (sigAlgebraβπ)) |
4 | | isldsys.l |
. . . . . . . 8
β’ πΏ = {π β π« π« π β£ (β
β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} |
5 | 4 | sigaldsys 32822 |
. . . . . . 7
β’
(sigAlgebraβπ)
β πΏ |
6 | 5, 3 | sselid 3946 |
. . . . . 6
β’ (π β π« π β πΏ) |
7 | | ldsysgenld.2 |
. . . . . 6
β’ (π β π΄ β π« π) |
8 | | sseq2 3974 |
. . . . . . 7
β’ (π‘ = π« π β (π΄ β π‘ β π΄ β π« π)) |
9 | 8 | elrab 3649 |
. . . . . 6
β’
(π« π β
{π‘ β πΏ β£ π΄ β π‘} β (π« π β πΏ β§ π΄ β π« π)) |
10 | 6, 7, 9 | sylanbrc 584 |
. . . . 5
β’ (π β π« π β {π‘ β πΏ β£ π΄ β π‘}) |
11 | | intss1 4928 |
. . . . 5
β’
(π« π β
{π‘ β πΏ β£ π΄ β π‘} β β© {π‘ β πΏ β£ π΄ β π‘} β π« π) |
12 | 10, 11 | syl 17 |
. . . 4
β’ (π β β© {π‘
β πΏ β£ π΄ β π‘} β π« π) |
13 | 3, 12 | sselpwd 5287 |
. . 3
β’ (π β β© {π‘
β πΏ β£ π΄ β π‘} β π« π« π) |
14 | 4 | isldsys 32819 |
. . . . . . . . . 10
β’ (π‘ β πΏ β (π‘ β π« π« π β§ (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)))) |
15 | 14 | simprbi 498 |
. . . . . . . . 9
β’ (π‘ β πΏ β (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘))) |
16 | 15 | simp1d 1143 |
. . . . . . . 8
β’ (π‘ β πΏ β β
β π‘) |
17 | 16 | adantl 483 |
. . . . . . 7
β’ ((π β§ π‘ β πΏ) β β
β π‘) |
18 | 17 | a1d 25 |
. . . . . 6
β’ ((π β§ π‘ β πΏ) β (π΄ β π‘ β β
β π‘)) |
19 | 18 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ‘ β πΏ (π΄ β π‘ β β
β π‘)) |
20 | | 0ex 5268 |
. . . . . 6
β’ β
β V |
21 | 20 | elintrab 4925 |
. . . . 5
β’ (β
β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β β
β π‘)) |
22 | 19, 21 | sylibr 233 |
. . . 4
β’ (π β β
β β© {π‘
β πΏ β£ π΄ β π‘}) |
23 | | nfv 1918 |
. . . . . . . 8
β’
β²π‘π |
24 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π‘π₯ |
25 | | nfrab1 3425 |
. . . . . . . . . 10
β’
β²π‘{π‘ β πΏ β£ π΄ β π‘} |
26 | 25 | nfint 4921 |
. . . . . . . . 9
β’
β²π‘β© {π‘
β πΏ β£ π΄ β π‘} |
27 | 24, 26 | nfel 2918 |
. . . . . . . 8
β’
β²π‘ π₯ β β© {π‘
β πΏ β£ π΄ β π‘} |
28 | 23, 27 | nfan 1903 |
. . . . . . 7
β’
β²π‘(π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) |
29 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β§ π΄ β π‘) β π‘ β πΏ) |
30 | | vex 3451 |
. . . . . . . . . . . . . . 15
β’ π₯ β V |
31 | 30 | elintrab 4925 |
. . . . . . . . . . . . . 14
β’ (π₯ β β© {π‘
β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β π₯ β π‘)) |
32 | 31 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π₯ β β© {π‘
β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β π₯ β π‘)) |
33 | 32 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β βπ‘ β πΏ (π΄ β π‘ β π₯ β π‘)) |
34 | 33 | r19.21bi 3233 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β (π΄ β π‘ β π₯ β π‘)) |
35 | 34 | imp 408 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β§ π΄ β π‘) β π₯ β π‘) |
36 | 15 | simp2d 1144 |
. . . . . . . . . . 11
β’ (π‘ β πΏ β βπ₯ β π‘ (π β π₯) β π‘) |
37 | 36 | r19.21bi 3233 |
. . . . . . . . . 10
β’ ((π‘ β πΏ β§ π₯ β π‘) β (π β π₯) β π‘) |
38 | 29, 35, 37 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β§ π΄ β π‘) β (π β π₯) β π‘) |
39 | 38 | ex 414 |
. . . . . . . 8
β’ (((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β (π΄ β π‘ β (π β π₯) β π‘)) |
40 | 39 | ex 414 |
. . . . . . 7
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β (π‘ β πΏ β (π΄ β π‘ β (π β π₯) β π‘))) |
41 | 28, 40 | ralrimi 3239 |
. . . . . 6
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β βπ‘ β πΏ (π΄ β π‘ β (π β π₯) β π‘)) |
42 | | difexg 5288 |
. . . . . . . 8
β’ (π β π β (π β π₯) β V) |
43 | | elintrabg 4926 |
. . . . . . . 8
β’ ((π β π₯) β V β ((π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β (π β π₯) β π‘))) |
44 | 1, 42, 43 | 3syl 18 |
. . . . . . 7
β’ (π β ((π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β (π β π₯) β π‘))) |
45 | 44 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β ((π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β (π β π₯) β π‘))) |
46 | 41, 45 | mpbird 257 |
. . . . 5
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘}) |
47 | 46 | ralrimiva 3140 |
. . . 4
β’ (π β βπ₯ β β© {π‘ β πΏ β£ π΄ β π‘} (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘}) |
48 | 26 | nfpw 4583 |
. . . . . . . . . . 11
β’
β²π‘π« β© {π‘ β πΏ β£ π΄ β π‘} |
49 | 24, 48 | nfel 2918 |
. . . . . . . . . 10
β’
β²π‘ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} |
50 | 23, 49 | nfan 1903 |
. . . . . . . . 9
β’
β²π‘(π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) |
51 | | nfv 1918 |
. . . . . . . . 9
β’
β²π‘(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦) |
52 | 50, 51 | nfan 1903 |
. . . . . . . 8
β’
β²π‘((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) |
53 | | simplr 768 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β π‘ β πΏ) |
54 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β§ π’ β β© {π‘ β πΏ β£ π΄ β π‘}) β π’ β β© {π‘ β πΏ β£ π΄ β π‘}) |
55 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β§ π’ β β© {π‘ β πΏ β£ π΄ β π‘}) β π‘ β πΏ) |
56 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β§ π’ β β© {π‘ β πΏ β£ π΄ β π‘}) β π΄ β π‘) |
57 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . 20
β’ π’ β V |
58 | 57 | elintrab 4925 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β β© {π‘
β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β π’ β π‘)) |
59 | 58 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β β© {π‘
β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β π’ β π‘)) |
60 | 59 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β β© {π‘
β πΏ β£ π΄ β π‘} β§ π‘ β πΏ) β (π΄ β π‘ β π’ β π‘)) |
61 | 60 | imp 408 |
. . . . . . . . . . . . . . . 16
β’ (((π’ β β© {π‘
β πΏ β£ π΄ β π‘} β§ π‘ β πΏ) β§ π΄ β π‘) β π’ β π‘) |
62 | 54, 55, 56, 61 | syl21anc 837 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β§ π’ β β© {π‘ β πΏ β£ π΄ β π‘}) β π’ β π‘) |
63 | 62 | ex 414 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β (π’ β β© {π‘ β πΏ β£ π΄ β π‘} β π’ β π‘)) |
64 | 63 | ssrdv 3954 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β β© {π‘ β πΏ β£ π΄ β π‘} β π‘) |
65 | 64 | sspwd 4577 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β π« β© {π‘
β πΏ β£ π΄ β π‘} β π« π‘) |
66 | | simp-4r 783 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) |
67 | 65, 66 | sseldd 3949 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β π₯ β π« π‘) |
68 | | simpllr 775 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) |
69 | 15 | simp3d 1145 |
. . . . . . . . . . . . 13
β’ (π‘ β πΏ β βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) |
70 | 69 | r19.21bi 3233 |
. . . . . . . . . . . 12
β’ ((π‘ β πΏ β§ π₯ β π« π‘) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) |
71 | 70 | imp 408 |
. . . . . . . . . . 11
β’ (((π‘ β πΏ β§ π₯ β π« π‘) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β βͺ π₯ β π‘) |
72 | 53, 67, 68, 71 | syl21anc 837 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β βͺ π₯ β π‘) |
73 | 72 | ex 414 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β (π΄ β π‘ β βͺ π₯ β π‘)) |
74 | 73 | ex 414 |
. . . . . . . 8
β’ (((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β (π‘ β πΏ β (π΄ β π‘ β βͺ π₯ β π‘))) |
75 | 52, 74 | ralrimi 3239 |
. . . . . . 7
β’ (((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β βπ‘ β πΏ (π΄ β π‘ β βͺ π₯ β π‘)) |
76 | | vuniex 7680 |
. . . . . . . 8
β’ βͺ π₯
β V |
77 | 76 | elintrab 4925 |
. . . . . . 7
β’ (βͺ π₯
β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β βͺ π₯ β π‘)) |
78 | 75, 77 | sylibr 233 |
. . . . . 6
β’ (((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘}) |
79 | 78 | ex 414 |
. . . . 5
β’ ((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘})) |
80 | 79 | ralrimiva 3140 |
. . . 4
β’ (π β βπ₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘})) |
81 | 22, 47, 80 | 3jca 1129 |
. . 3
β’ (π β (β
β β© {π‘
β πΏ β£ π΄ β π‘} β§ βπ₯ β β© {π‘ β πΏ β£ π΄ β π‘} (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β§ βπ₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘}))) |
82 | 13, 81 | jca 513 |
. 2
β’ (π β (β© {π‘
β πΏ β£ π΄ β π‘} β π« π« π β§ (β
β β© {π‘
β πΏ β£ π΄ β π‘} β§ βπ₯ β β© {π‘ β πΏ β£ π΄ β π‘} (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β§ βπ₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘})))) |
83 | 4 | isldsys 32819 |
. 2
β’ (β© {π‘
β πΏ β£ π΄ β π‘} β πΏ β (β© {π‘ β πΏ β£ π΄ β π‘} β π« π« π β§ (β
β β© {π‘
β πΏ β£ π΄ β π‘} β§ βπ₯ β β© {π‘ β πΏ β£ π΄ β π‘} (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β§ βπ₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘})))) |
84 | 82, 83 | sylibr 233 |
1
β’ (π β β© {π‘
β πΏ β£ π΄ β π‘} β πΏ) |