Step | Hyp | Ref
| Expression |
1 | | intex 4820 |
. . . 4
|
2 | 1 | biimpi 206 |
. . 3
|
3 | 2 | adantr 481 |
. 2
sigAlgebra |
4 | | intssuni 4499 |
. . . 4
|
5 | 4 | adantr 481 |
. . 3
sigAlgebra |
6 | | simpr 477 |
. . . . 5
sigAlgebra sigAlgebra |
7 | | elpwi 4168 |
. . . . . 6
sigAlgebra
sigAlgebra |
8 | | sigasspw 30179 |
. . . . . . . 8
sigAlgebra
|
9 | | selpw 4165 |
. . . . . . . 8
|
10 | 8, 9 | sylibr 224 |
. . . . . . 7
sigAlgebra |
11 | 10 | ssriv 3607 |
. . . . . 6
sigAlgebra
|
12 | 7, 11 | syl6ss 3615 |
. . . . 5
sigAlgebra
|
13 | 6, 12 | syl 17 |
. . . 4
sigAlgebra |
14 | | sspwuni 4611 |
. . . 4
|
15 | 13, 14 | sylib 208 |
. . 3
sigAlgebra |
16 | 5, 15 | sstrd 3613 |
. 2
sigAlgebra |
17 | | simpr 477 |
. . . . . . . . 9
sigAlgebra
|
18 | | simplr 792 |
. . . . . . . . 9
sigAlgebra
sigAlgebra |
19 | | elelpwi 4171 |
. . . . . . . . 9
sigAlgebra sigAlgebra |
20 | 17, 18, 19 | syl2anc 693 |
. . . . . . . 8
sigAlgebra
sigAlgebra |
21 | | vex 3203 |
. . . . . . . . 9
|
22 | | issiga 30174 |
. . . . . . . . 9
sigAlgebra
|
23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
sigAlgebra
|
24 | 20, 23 | sylib 208 |
. . . . . . 7
sigAlgebra
|
25 | 24 | simprd 479 |
. . . . . 6
sigAlgebra
|
26 | 25 | simp1d 1073 |
. . . . 5
sigAlgebra
|
27 | 26 | ralrimiva 2966 |
. . . 4
sigAlgebra
|
28 | | n0 3931 |
. . . . . . . . 9
|
29 | 28 | biimpi 206 |
. . . . . . . 8
|
30 | 29 | adantr 481 |
. . . . . . 7
sigAlgebra |
31 | 20 | ex 450 |
. . . . . . . 8
sigAlgebra
sigAlgebra |
32 | 31 | eximdv 1846 |
. . . . . . 7
sigAlgebra
sigAlgebra |
33 | 30, 32 | mpd 15 |
. . . . . 6
sigAlgebra sigAlgebra |
34 | | elfvex 6221 |
. . . . . . 7
sigAlgebra
|
35 | 34 | exlimiv 1858 |
. . . . . 6
sigAlgebra |
36 | 33, 35 | syl 17 |
. . . . 5
sigAlgebra |
37 | | elintg 4483 |
. . . . 5
|
38 | 36, 37 | syl 17 |
. . . 4
sigAlgebra
|
39 | 27, 38 | mpbird 247 |
. . 3
sigAlgebra |
40 | | simpll 790 |
. . . . . . . 8
sigAlgebra sigAlgebra |
41 | | simpr 477 |
. . . . . . . 8
sigAlgebra |
42 | 40, 41 | jca 554 |
. . . . . . 7
sigAlgebra sigAlgebra |
43 | | elinti 4485 |
. . . . . . . . 9
|
44 | 43 | imp 445 |
. . . . . . . 8
|
45 | 44 | adantll 750 |
. . . . . . 7
sigAlgebra |
46 | 25 | simp2d 1074 |
. . . . . . . 8
sigAlgebra
|
47 | 46 | r19.21bi 2932 |
. . . . . . 7
sigAlgebra
|
48 | 42, 45, 47 | syl2anc 693 |
. . . . . 6
sigAlgebra |
49 | 48 | ralrimiva 2966 |
. . . . 5
sigAlgebra
|
50 | | difexg 4808 |
. . . . . . . 8
|
51 | 36, 50 | syl 17 |
. . . . . . 7
sigAlgebra |
52 | 51 | adantr 481 |
. . . . . 6
sigAlgebra |
53 | | elintg 4483 |
. . . . . 6
|
54 | 52, 53 | syl 17 |
. . . . 5
sigAlgebra |
55 | 49, 54 | mpbird 247 |
. . . 4
sigAlgebra |
56 | 55 | ralrimiva 2966 |
. . 3
sigAlgebra |
57 | | simplll 798 |
. . . . . . . . . 10
sigAlgebra
sigAlgebra |
58 | | simpr 477 |
. . . . . . . . . 10
sigAlgebra
|
59 | 57, 58 | jca 554 |
. . . . . . . . 9
sigAlgebra
sigAlgebra |
60 | | simpllr 799 |
. . . . . . . . . 10
sigAlgebra
|
61 | | elpwi 4168 |
. . . . . . . . . . . 12
|
62 | | intss1 4492 |
. . . . . . . . . . . 12
|
63 | 61, 62 | sylan9ss 3616 |
. . . . . . . . . . 11
|
64 | | selpw 4165 |
. . . . . . . . . . 11
|
65 | 63, 64 | sylibr 224 |
. . . . . . . . . 10
|
66 | 60, 65 | sylancom 701 |
. . . . . . . . 9
sigAlgebra
|
67 | 59, 66 | jca 554 |
. . . . . . . 8
sigAlgebra
sigAlgebra
|
68 | | simplr 792 |
. . . . . . . 8
sigAlgebra
|
69 | 25 | simp3d 1075 |
. . . . . . . . 9
sigAlgebra
|
70 | 69 | r19.21bi 2932 |
. . . . . . . 8
sigAlgebra
|
71 | 67, 68, 70 | sylc 65 |
. . . . . . 7
sigAlgebra
|
72 | 71 | ralrimiva 2966 |
. . . . . 6
sigAlgebra
|
73 | | uniexg 6955 |
. . . . . . . 8
|
74 | 73 | ad2antlr 763 |
. . . . . . 7
sigAlgebra
|
75 | | elintg 4483 |
. . . . . . 7
|
76 | 74, 75 | syl 17 |
. . . . . 6
sigAlgebra
|
77 | 72, 76 | mpbird 247 |
. . . . 5
sigAlgebra
|
78 | 77 | ex 450 |
. . . 4
sigAlgebra
|
79 | 78 | ralrimiva 2966 |
. . 3
sigAlgebra |
80 | 39, 56, 79 | 3jca 1242 |
. 2
sigAlgebra
|
81 | | issiga 30174 |
. . 3
sigAlgebra
|
82 | 81 | biimpar 502 |
. 2
sigAlgebra |
83 | 3, 16, 80, 82 | syl12anc 1324 |
1
sigAlgebra sigAlgebra |