Step | Hyp | Ref
| Expression |
1 | | ldsysgenld.1 |
. . . . 5
β’ (π β π β π) |
2 | | pwsiga 33123 |
. . . . 5
β’ (π β π β π« π β (sigAlgebraβπ)) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π« π β (sigAlgebraβπ)) |
4 | | isldsys.l |
. . . . . . . 8
β’ πΏ = {π β π« π« π β£ (β
β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π ))} |
5 | 4 | sigaldsys 33152 |
. . . . . . 7
β’
(sigAlgebraβπ)
β πΏ |
6 | 5, 3 | sselid 3980 |
. . . . . 6
β’ (π β π« π β πΏ) |
7 | | ldsysgenld.2 |
. . . . . 6
β’ (π β π΄ β π« π) |
8 | | sseq2 4008 |
. . . . . . 7
β’ (π‘ = π« π β (π΄ β π‘ β π΄ β π« π)) |
9 | 8 | elrab 3683 |
. . . . . 6
β’
(π« π β
{π‘ β πΏ β£ π΄ β π‘} β (π« π β πΏ β§ π΄ β π« π)) |
10 | 6, 7, 9 | sylanbrc 583 |
. . . . 5
β’ (π β π« π β {π‘ β πΏ β£ π΄ β π‘}) |
11 | | intss1 4967 |
. . . . 5
β’
(π« π β
{π‘ β πΏ β£ π΄ β π‘} β β© {π‘ β πΏ β£ π΄ β π‘} β π« π) |
12 | 10, 11 | syl 17 |
. . . 4
β’ (π β β© {π‘
β πΏ β£ π΄ β π‘} β π« π) |
13 | 3, 12 | sselpwd 5326 |
. . 3
β’ (π β β© {π‘
β πΏ β£ π΄ β π‘} β π« π« π) |
14 | 4 | isldsys 33149 |
. . . . . . . . . 10
β’ (π‘ β πΏ β (π‘ β π« π« π β§ (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)))) |
15 | 14 | simprbi 497 |
. . . . . . . . 9
β’ (π‘ β πΏ β (β
β π‘ β§ βπ₯ β π‘ (π β π₯) β π‘ β§ βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘))) |
16 | 15 | simp1d 1142 |
. . . . . . . 8
β’ (π‘ β πΏ β β
β π‘) |
17 | 16 | adantl 482 |
. . . . . . 7
β’ ((π β§ π‘ β πΏ) β β
β π‘) |
18 | 17 | a1d 25 |
. . . . . 6
β’ ((π β§ π‘ β πΏ) β (π΄ β π‘ β β
β π‘)) |
19 | 18 | ralrimiva 3146 |
. . . . 5
β’ (π β βπ‘ β πΏ (π΄ β π‘ β β
β π‘)) |
20 | | 0ex 5307 |
. . . . . 6
β’ β
β V |
21 | 20 | elintrab 4964 |
. . . . 5
β’ (β
β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β β
β π‘)) |
22 | 19, 21 | sylibr 233 |
. . . 4
β’ (π β β
β β© {π‘
β πΏ β£ π΄ β π‘}) |
23 | | nfv 1917 |
. . . . . . . 8
β’
β²π‘π |
24 | | nfcv 2903 |
. . . . . . . . 9
β’
β²π‘π₯ |
25 | | nfrab1 3451 |
. . . . . . . . . 10
β’
β²π‘{π‘ β πΏ β£ π΄ β π‘} |
26 | 25 | nfint 4960 |
. . . . . . . . 9
β’
β²π‘β© {π‘
β πΏ β£ π΄ β π‘} |
27 | 24, 26 | nfel 2917 |
. . . . . . . 8
β’
β²π‘ π₯ β β© {π‘
β πΏ β£ π΄ β π‘} |
28 | 23, 27 | nfan 1902 |
. . . . . . 7
β’
β²π‘(π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) |
29 | | simplr 767 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β§ π΄ β π‘) β π‘ β πΏ) |
30 | | vex 3478 |
. . . . . . . . . . . . . . 15
β’ π₯ β V |
31 | 30 | elintrab 4964 |
. . . . . . . . . . . . . 14
β’ (π₯ β β© {π‘
β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β π₯ β π‘)) |
32 | 31 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π₯ β β© {π‘
β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β π₯ β π‘)) |
33 | 32 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β βπ‘ β πΏ (π΄ β π‘ β π₯ β π‘)) |
34 | 33 | r19.21bi 3248 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β (π΄ β π‘ β π₯ β π‘)) |
35 | 34 | imp 407 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β§ π΄ β π‘) β π₯ β π‘) |
36 | 15 | simp2d 1143 |
. . . . . . . . . . 11
β’ (π‘ β πΏ β βπ₯ β π‘ (π β π₯) β π‘) |
37 | 36 | r19.21bi 3248 |
. . . . . . . . . 10
β’ ((π‘ β πΏ β§ π₯ β π‘) β (π β π₯) β π‘) |
38 | 29, 35, 37 | syl2anc 584 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β§ π΄ β π‘) β (π β π₯) β π‘) |
39 | 38 | ex 413 |
. . . . . . . 8
β’ (((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β§ π‘ β πΏ) β (π΄ β π‘ β (π β π₯) β π‘)) |
40 | 39 | ex 413 |
. . . . . . 7
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β (π‘ β πΏ β (π΄ β π‘ β (π β π₯) β π‘))) |
41 | 28, 40 | ralrimi 3254 |
. . . . . 6
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β βπ‘ β πΏ (π΄ β π‘ β (π β π₯) β π‘)) |
42 | | difexg 5327 |
. . . . . . . 8
β’ (π β π β (π β π₯) β V) |
43 | | elintrabg 4965 |
. . . . . . . 8
β’ ((π β π₯) β V β ((π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β (π β π₯) β π‘))) |
44 | 1, 42, 43 | 3syl 18 |
. . . . . . 7
β’ (π β ((π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β (π β π₯) β π‘))) |
45 | 44 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β ((π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β (π β π₯) β π‘))) |
46 | 41, 45 | mpbird 256 |
. . . . 5
β’ ((π β§ π₯ β β© {π‘ β πΏ β£ π΄ β π‘}) β (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘}) |
47 | 46 | ralrimiva 3146 |
. . . 4
β’ (π β βπ₯ β β© {π‘ β πΏ β£ π΄ β π‘} (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘}) |
48 | 26 | nfpw 4621 |
. . . . . . . . . . 11
β’
β²π‘π« β© {π‘ β πΏ β£ π΄ β π‘} |
49 | 24, 48 | nfel 2917 |
. . . . . . . . . 10
β’
β²π‘ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} |
50 | 23, 49 | nfan 1902 |
. . . . . . . . 9
β’
β²π‘(π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) |
51 | | nfv 1917 |
. . . . . . . . 9
β’
β²π‘(π₯ βΌ Ο β§
Disj π¦ β π₯ π¦) |
52 | 50, 51 | nfan 1902 |
. . . . . . . 8
β’
β²π‘((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) |
53 | | simplr 767 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β π‘ β πΏ) |
54 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β§ π’ β β© {π‘ β πΏ β£ π΄ β π‘}) β π’ β β© {π‘ β πΏ β£ π΄ β π‘}) |
55 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β§ π’ β β© {π‘ β πΏ β£ π΄ β π‘}) β π‘ β πΏ) |
56 | | simplr 767 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β§ π’ β β© {π‘ β πΏ β£ π΄ β π‘}) β π΄ β π‘) |
57 | | vex 3478 |
. . . . . . . . . . . . . . . . . . . 20
β’ π’ β V |
58 | 57 | elintrab 4964 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β β© {π‘
β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β π’ β π‘)) |
59 | 58 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β β© {π‘
β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β π’ β π‘)) |
60 | 59 | r19.21bi 3248 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β β© {π‘
β πΏ β£ π΄ β π‘} β§ π‘ β πΏ) β (π΄ β π‘ β π’ β π‘)) |
61 | 60 | imp 407 |
. . . . . . . . . . . . . . . 16
β’ (((π’ β β© {π‘
β πΏ β£ π΄ β π‘} β§ π‘ β πΏ) β§ π΄ β π‘) β π’ β π‘) |
62 | 54, 55, 56, 61 | syl21anc 836 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β§ π’ β β© {π‘ β πΏ β£ π΄ β π‘}) β π’ β π‘) |
63 | 62 | ex 413 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β (π’ β β© {π‘ β πΏ β£ π΄ β π‘} β π’ β π‘)) |
64 | 63 | ssrdv 3988 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β β© {π‘ β πΏ β£ π΄ β π‘} β π‘) |
65 | 64 | sspwd 4615 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β π« β© {π‘
β πΏ β£ π΄ β π‘} β π« π‘) |
66 | | simp-4r 782 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) |
67 | 65, 66 | sseldd 3983 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β π₯ β π« π‘) |
68 | | simpllr 774 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) |
69 | 15 | simp3d 1144 |
. . . . . . . . . . . . 13
β’ (π‘ β πΏ β βπ₯ β π« π‘((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) |
70 | 69 | r19.21bi 3248 |
. . . . . . . . . . . 12
β’ ((π‘ β πΏ β§ π₯ β π« π‘) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β π‘)) |
71 | 70 | imp 407 |
. . . . . . . . . . 11
β’ (((π‘ β πΏ β§ π₯ β π« π‘) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β βͺ π₯ β π‘) |
72 | 53, 67, 68, 71 | syl21anc 836 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β§ π΄ β π‘) β βͺ π₯ β π‘) |
73 | 72 | ex 413 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β§ π‘ β πΏ) β (π΄ β π‘ β βͺ π₯ β π‘)) |
74 | 73 | ex 413 |
. . . . . . . 8
β’ (((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β (π‘ β πΏ β (π΄ β π‘ β βͺ π₯ β π‘))) |
75 | 52, 74 | ralrimi 3254 |
. . . . . . 7
β’ (((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β βπ‘ β πΏ (π΄ β π‘ β βͺ π₯ β π‘)) |
76 | | vuniex 7728 |
. . . . . . . 8
β’ βͺ π₯
β V |
77 | 76 | elintrab 4964 |
. . . . . . 7
β’ (βͺ π₯
β β© {π‘ β πΏ β£ π΄ β π‘} β βπ‘ β πΏ (π΄ β π‘ β βͺ π₯ β π‘)) |
78 | 75, 77 | sylibr 233 |
. . . . . 6
β’ (((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β§ (π₯ βΌ Ο β§ Disj π¦ β π₯ π¦)) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘}) |
79 | 78 | ex 413 |
. . . . 5
β’ ((π β§ π₯ β π« β© {π‘
β πΏ β£ π΄ β π‘}) β ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘})) |
80 | 79 | ralrimiva 3146 |
. . . 4
β’ (π β βπ₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘})) |
81 | 22, 47, 80 | 3jca 1128 |
. . 3
β’ (π β (β
β β© {π‘
β πΏ β£ π΄ β π‘} β§ βπ₯ β β© {π‘ β πΏ β£ π΄ β π‘} (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β§ βπ₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘}))) |
82 | 13, 81 | jca 512 |
. 2
β’ (π β (β© {π‘
β πΏ β£ π΄ β π‘} β π« π« π β§ (β
β β© {π‘
β πΏ β£ π΄ β π‘} β§ βπ₯ β β© {π‘ β πΏ β£ π΄ β π‘} (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β§ βπ₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘})))) |
83 | 4 | isldsys 33149 |
. 2
β’ (β© {π‘
β πΏ β£ π΄ β π‘} β πΏ β (β© {π‘ β πΏ β£ π΄ β π‘} β π« π« π β§ (β
β β© {π‘
β πΏ β£ π΄ β π‘} β§ βπ₯ β β© {π‘ β πΏ β£ π΄ β π‘} (π β π₯) β β© {π‘ β πΏ β£ π΄ β π‘} β§ βπ₯ β π« β© {π‘
β πΏ β£ π΄ β π‘} ((π₯ βΌ Ο β§ Disj π¦ β π₯ π¦) β βͺ π₯ β β© {π‘
β πΏ β£ π΄ β π‘})))) |
84 | 82, 83 | sylibr 233 |
1
β’ (π β β© {π‘
β πΏ β£ π΄ β π‘} β πΏ) |