Step | Hyp | Ref
| Expression |
1 | | intex 5292 |
. . . 4
β’ (π΄ β β
β β© π΄
β V) |
2 | 1 | biimpi 215 |
. . 3
β’ (π΄ β β
β β© π΄
β V) |
3 | 2 | adantr 481 |
. 2
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β β© π΄ β V) |
4 | | intssuni 4929 |
. . . 4
β’ (π΄ β β
β β© π΄
β βͺ π΄) |
5 | 4 | adantr 481 |
. . 3
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β β© π΄ β βͺ π΄) |
6 | | simpr 485 |
. . . . 5
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β π΄ β π«
(sigAlgebraβπ)) |
7 | | elpwi 4565 |
. . . . . 6
β’ (π΄ β π«
(sigAlgebraβπ) β
π΄ β
(sigAlgebraβπ)) |
8 | | sigasspw 32584 |
. . . . . . . 8
β’ (π β (sigAlgebraβπ) β π β π« π) |
9 | | velpw 4563 |
. . . . . . . 8
β’ (π β π« π«
π β π β π« π) |
10 | 8, 9 | sylibr 233 |
. . . . . . 7
β’ (π β (sigAlgebraβπ) β π β π« π« π) |
11 | 10 | ssriv 3946 |
. . . . . 6
β’
(sigAlgebraβπ)
β π« π« π |
12 | 7, 11 | sstrdi 3954 |
. . . . 5
β’ (π΄ β π«
(sigAlgebraβπ) β
π΄ β π«
π« π) |
13 | 6, 12 | syl 17 |
. . . 4
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β π΄ β π«
π« π) |
14 | | sspwuni 5058 |
. . . 4
β’ (π΄ β π« π«
π β βͺ π΄
β π« π) |
15 | 13, 14 | sylib 217 |
. . 3
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β βͺ π΄ β π« π) |
16 | 5, 15 | sstrd 3952 |
. 2
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β β© π΄ β π« π) |
17 | | simpr 485 |
. . . . . . . . 9
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β π β π΄) |
18 | | simplr 767 |
. . . . . . . . 9
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β π΄ β π« (sigAlgebraβπ)) |
19 | | elelpwi 4568 |
. . . . . . . . 9
β’ ((π β π΄ β§ π΄ β π« (sigAlgebraβπ)) β π β (sigAlgebraβπ)) |
20 | 17, 18, 19 | syl2anc 584 |
. . . . . . . 8
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β π β (sigAlgebraβπ)) |
21 | | vex 3447 |
. . . . . . . . 9
β’ π β V |
22 | | issiga 32580 |
. . . . . . . . 9
β’ (π β V β (π β (sigAlgebraβπ) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))))) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
β’ (π β (sigAlgebraβπ) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))) |
24 | 20, 23 | sylib 217 |
. . . . . . 7
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))) |
25 | 24 | simprd 496 |
. . . . . 6
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))) |
26 | 25 | simp1d 1142 |
. . . . 5
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β π β π ) |
27 | 26 | ralrimiva 3141 |
. . . 4
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β βπ β
π΄ π β π ) |
28 | | n0 4304 |
. . . . . . . . 9
β’ (π΄ β β
β
βπ π β π΄) |
29 | 28 | biimpi 215 |
. . . . . . . 8
β’ (π΄ β β
β
βπ π β π΄) |
30 | 29 | adantr 481 |
. . . . . . 7
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β βπ π β π΄) |
31 | 20 | ex 413 |
. . . . . . . 8
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β (π β π΄ β π β (sigAlgebraβπ))) |
32 | 31 | eximdv 1920 |
. . . . . . 7
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β (βπ π β π΄ β βπ π β (sigAlgebraβπ))) |
33 | 30, 32 | mpd 15 |
. . . . . 6
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β βπ π β (sigAlgebraβπ)) |
34 | | elfvex 6877 |
. . . . . . 7
β’ (π β (sigAlgebraβπ) β π β V) |
35 | 34 | exlimiv 1933 |
. . . . . 6
β’
(βπ π β (sigAlgebraβπ) β π β V) |
36 | 33, 35 | syl 17 |
. . . . 5
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β π β
V) |
37 | | elintg 4913 |
. . . . 5
β’ (π β V β (π β β© π΄
β βπ β
π΄ π β π )) |
38 | 36, 37 | syl 17 |
. . . 4
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β (π β β© π΄
β βπ β
π΄ π β π )) |
39 | 27, 38 | mpbird 256 |
. . 3
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β π β β© π΄) |
40 | | simpll 765 |
. . . . . . . 8
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β§ π β π΄) β (π΄ β β
β§ π΄ β π« (sigAlgebraβπ))) |
41 | | simpr 485 |
. . . . . . . 8
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β§ π β π΄) β π β π΄) |
42 | 40, 41 | jca 512 |
. . . . . . 7
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β§ π β π΄) β ((π΄ β β
β§ π΄ β π« (sigAlgebraβπ)) β§ π β π΄)) |
43 | | elinti 4914 |
. . . . . . . . 9
β’ (π₯ β β© π΄
β (π β π΄ β π₯ β π )) |
44 | 43 | imp 407 |
. . . . . . . 8
β’ ((π₯ β β© π΄
β§ π β π΄) β π₯ β π ) |
45 | 44 | adantll 712 |
. . . . . . 7
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β§ π β π΄) β π₯ β π ) |
46 | 25 | simp2d 1143 |
. . . . . . . 8
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β βπ₯ β π (π β π₯) β π ) |
47 | 46 | r19.21bi 3232 |
. . . . . . 7
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β§ π₯ β π ) β (π β π₯) β π ) |
48 | 42, 45, 47 | syl2anc 584 |
. . . . . 6
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β§ π β π΄) β (π β π₯) β π ) |
49 | 48 | ralrimiva 3141 |
. . . . 5
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β βπ β
π΄ (π β π₯) β π ) |
50 | 36 | difexd 5284 |
. . . . . . 7
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β (π β π₯) β V) |
51 | 50 | adantr 481 |
. . . . . 6
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β (π β π₯) β V) |
52 | | elintg 4913 |
. . . . . 6
β’ ((π β π₯) β V β ((π β π₯) β β© π΄ β βπ β π΄ (π β π₯) β π )) |
53 | 51, 52 | syl 17 |
. . . . 5
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β ((π β π₯) β β© π΄
β βπ β
π΄ (π β π₯) β π )) |
54 | 49, 53 | mpbird 256 |
. . . 4
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β β© π΄)
β (π β π₯) β β© π΄) |
55 | 54 | ralrimiva 3141 |
. . 3
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β βπ₯ β
β© π΄(π β π₯) β β© π΄) |
56 | | simplll 773 |
. . . . . . . . . 10
β’
(((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β§ π β π΄) β (π΄ β β
β§ π΄ β π« (sigAlgebraβπ))) |
57 | | simpr 485 |
. . . . . . . . . 10
β’
(((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β§ π β π΄) β π β π΄) |
58 | 56, 57 | jca 512 |
. . . . . . . . 9
β’
(((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β§ π β π΄) β ((π΄ β β
β§ π΄ β π« (sigAlgebraβπ)) β§ π β π΄)) |
59 | | simpllr 774 |
. . . . . . . . . 10
β’
(((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β§ π β π΄) β π₯ β π« β© π΄) |
60 | | elpwi 4565 |
. . . . . . . . . . . 12
β’ (π₯ β π« β© π΄
β π₯ β β© π΄) |
61 | | intss1 4922 |
. . . . . . . . . . . 12
β’ (π β π΄ β β© π΄ β π ) |
62 | 60, 61 | sylan9ss 3955 |
. . . . . . . . . . 11
β’ ((π₯ β π« β© π΄
β§ π β π΄) β π₯ β π ) |
63 | | velpw 4563 |
. . . . . . . . . . 11
β’ (π₯ β π« π β π₯ β π ) |
64 | 62, 63 | sylibr 233 |
. . . . . . . . . 10
β’ ((π₯ β π« β© π΄
β§ π β π΄) β π₯ β π« π ) |
65 | 59, 64 | sylancom 588 |
. . . . . . . . 9
β’
(((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β§ π β π΄) β π₯ β π« π ) |
66 | 58, 65 | jca 512 |
. . . . . . . 8
β’
(((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β§ π β π΄) β (((π΄ β β
β§ π΄ β π« (sigAlgebraβπ)) β§ π β π΄) β§ π₯ β π« π )) |
67 | | simplr 767 |
. . . . . . . 8
β’
(((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β§ π β π΄) β π₯ βΌ Ο) |
68 | 25 | simp3d 1144 |
. . . . . . . . 9
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )) |
69 | 68 | r19.21bi 3232 |
. . . . . . . 8
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π β π΄) β§ π₯ β π« π ) β (π₯ βΌ Ο β βͺ π₯
β π )) |
70 | 66, 67, 69 | sylc 65 |
. . . . . . 7
β’
(((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β§ π β π΄) β βͺ π₯
β π ) |
71 | 70 | ralrimiva 3141 |
. . . . . 6
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β βπ β
π΄ βͺ π₯
β π ) |
72 | | uniexg 7673 |
. . . . . . . 8
β’ (π₯ β π« β© π΄
β βͺ π₯ β V) |
73 | 72 | ad2antlr 725 |
. . . . . . 7
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β βͺ π₯ β V) |
74 | | elintg 4913 |
. . . . . . 7
β’ (βͺ π₯
β V β (βͺ π₯ β β© π΄ β βπ β π΄ βͺ π₯ β π )) |
75 | 73, 74 | syl 17 |
. . . . . 6
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β (βͺ π₯ β β© π΄ β βπ β π΄ βͺ π₯ β π )) |
76 | 71, 75 | mpbird 256 |
. . . . 5
β’ ((((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β§ π₯ βΌ Ο)
β βͺ π₯ β β© π΄) |
77 | 76 | ex 413 |
. . . 4
β’ (((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ)) β§
π₯ β π« β© π΄)
β (π₯ βΌ Ο
β βͺ π₯ β β© π΄)) |
78 | 77 | ralrimiva 3141 |
. . 3
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β βπ₯ β
π« β© π΄(π₯ βΌ Ο β βͺ π₯
β β© π΄)) |
79 | 39, 55, 78 | 3jca 1128 |
. 2
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β (π β β© π΄
β§ βπ₯ β
β© π΄(π β π₯) β β© π΄ β§ βπ₯ β π« β© π΄(π₯ βΌ Ο β βͺ π₯
β β© π΄))) |
80 | | issiga 32580 |
. . 3
β’ (β© π΄
β V β (β© π΄ β (sigAlgebraβπ) β (β© π΄ β π« π β§ (π β β© π΄ β§ βπ₯ β β© π΄(π β π₯) β β© π΄ β§ βπ₯ β π« β© π΄(π₯ βΌ Ο β βͺ π₯
β β© π΄))))) |
81 | 80 | biimpar 478 |
. 2
β’ ((β© π΄
β V β§ (β© π΄ β π« π β§ (π β β© π΄ β§ βπ₯ β β© π΄(π β π₯) β β© π΄ β§ βπ₯ β π« β© π΄(π₯ βΌ Ο β βͺ π₯
β β© π΄)))) β β©
π΄ β
(sigAlgebraβπ)) |
82 | 3, 16, 79, 81 | syl12anc 835 |
1
β’ ((π΄ β β
β§ π΄ β π«
(sigAlgebraβπ))
β β© π΄ β (sigAlgebraβπ)) |