Step | Hyp | Ref
| Expression |
1 | | dynkin.p |
. . . 4
|
2 | 1 | sigapisys 30218 |
. . 3
sigAlgebra
|
3 | | dynkin.l |
. . . 4
Disj
|
4 | 3 | sigaldsys 30222 |
. . 3
sigAlgebra
|
5 | 2, 4 | ssini 3836 |
. 2
sigAlgebra
|
6 | | id 22 |
. . . . . . . . 9
|
7 | 6 | elin1d 3802 |
. . . . . . . 8
|
8 | 1 | ispisys 30215 |
. . . . . . . 8
|
9 | 7, 8 | sylib 208 |
. . . . . . 7
|
10 | 9 | simpld 475 |
. . . . . 6
|
11 | 10 | elpwid 4170 |
. . . . 5
|
12 | | dif0 3950 |
. . . . . . 7
|
13 | 6 | elin2d 3803 |
. . . . . . . . . . 11
|
14 | 3 | isldsys 30219 |
. . . . . . . . . . 11
Disj
|
15 | 13, 14 | sylib 208 |
. . . . . . . . . 10
Disj
|
16 | 15 | simprd 479 |
. . . . . . . . 9
Disj
|
17 | 16 | simp2d 1074 |
. . . . . . . 8
|
18 | 16 | simp1d 1073 |
. . . . . . . . 9
|
19 | | difeq2 3722 |
. . . . . . . . . . 11
|
20 | | eqidd 2623 |
. . . . . . . . . . 11
|
21 | 19, 20 | eleq12d 2695 |
. . . . . . . . . 10
|
22 | 21 | rspcv 3305 |
. . . . . . . . 9
|
23 | 18, 22 | syl 17 |
. . . . . . . 8
|
24 | 17, 23 | mpd 15 |
. . . . . . 7
|
25 | 12, 24 | syl5eqelr 2706 |
. . . . . 6
|
26 | | unieq 4444 |
. . . . . . . . . . . 12
|
27 | | uni0 4465 |
. . . . . . . . . . . 12
|
28 | 26, 27 | syl6eq 2672 |
. . . . . . . . . . 11
|
29 | 28 | adantl 482 |
. . . . . . . . . 10
|
30 | 18 | ad3antrrr 766 |
. . . . . . . . . 10
|
31 | 29, 30 | eqeltrd 2701 |
. . . . . . . . 9
|
32 | | vex 3203 |
. . . . . . . . . . . . . 14
|
33 | 32 | 0sdom 8091 |
. . . . . . . . . . . . 13
|
34 | 33 | biimpri 218 |
. . . . . . . . . . . 12
|
35 | 34 | adantl 482 |
. . . . . . . . . . 11
|
36 | | simplr 792 |
. . . . . . . . . . . 12
|
37 | | nnenom 12779 |
. . . . . . . . . . . . 13
|
38 | 37 | ensymi 8006 |
. . . . . . . . . . . 12
|
39 | | domentr 8015 |
. . . . . . . . . . . 12
|
40 | 36, 38, 39 | sylancl 694 |
. . . . . . . . . . 11
|
41 | | fodomr 8111 |
. . . . . . . . . . 11
|
42 | 35, 40, 41 | syl2anc 693 |
. . . . . . . . . 10
|
43 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
44 | 43 | iundisj 23316 |
. . . . . . . . . . . . 13
..^ |
45 | | fofn 6117 |
. . . . . . . . . . . . . . 15
|
46 | | fniunfv 6505 |
. . . . . . . . . . . . . . 15
|
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
|
48 | | forn 6118 |
. . . . . . . . . . . . . . 15
|
49 | 48 | unieqd 4446 |
. . . . . . . . . . . . . 14
|
50 | 47, 49 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
51 | 44, 50 | syl5eqr 2670 |
. . . . . . . . . . . 12
..^ |
52 | 51 | adantl 482 |
. . . . . . . . . . 11
..^ |
53 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
54 | | difexg 4808 |
. . . . . . . . . . . . . 14
..^ |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . 13
..^ |
56 | 55 | dfiun3 5380 |
. . . . . . . . . . . 12
..^
..^ |
57 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
|
58 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
59 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
60 | 59 | nfrn 5368 |
. . . . . . . . . . . . . . . . . . 19
..^ |
61 | 58, 60 | nfel 2777 |
. . . . . . . . . . . . . . . . . 18
..^ |
62 | 57, 61 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
..^ |
63 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
..^
..^ ..^ |
64 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . 22
|
65 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
66 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
67 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
68 | | nfiu1 4550 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ |
69 | 67, 68 | nfdif 3731 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ |
70 | 66, 69 | nfmpt 4746 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ |
71 | 70 | nfrn 5368 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
72 | 65, 71 | nfel 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
73 | 64, 72 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
74 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | 73, 74 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
76 | 65, 69 | nfeq 2776 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
77 | 75, 76 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
78 | 6 | ad7antr 774 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
79 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . . . 22
|
80 | 79 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
|
81 | 80 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
82 | | fof 6115 |
. . . . . . . . . . . . . . . . . . . . . 22
|
83 | 82 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^ |
84 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
|
85 | 83, 84 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
86 | 81, 85 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
87 | | fzofi 12773 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ ..^ |
89 | 81 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^
..^ |
90 | 83 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
..^ |
91 | | fzossnn 12516 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
92 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
..^ ..^ |
93 | 92 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . 21
..^
..^
..^ |
94 | 90, 93 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^
..^ |
95 | 89, 94 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
..^
..^
..^ |
96 | 1, 3, 77, 78, 86, 88, 95 | sigapildsyslem 30224 |
. . . . . . . . . . . . . . . . . 18
..^
..^
..^ |
97 | 63, 96 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
98 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
99 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
100 | 99, 55 | elrnmpti 5376 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
101 | 98, 100 | sylib 208 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
102 | 62, 97, 101 | r19.29af 3076 |
. . . . . . . . . . . . . . . 16
..^ |
103 | 102 | ex 450 |
. . . . . . . . . . . . . . 15
..^
|
104 | 103 | ssrdv 3609 |
. . . . . . . . . . . . . 14
..^
|
105 | | nnex 11026 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | mptex 6486 |
. . . . . . . . . . . . . . . 16
..^ |
107 | 106 | rnex 7100 |
. . . . . . . . . . . . . . 15
..^ |
108 | | elpwg 4166 |
. . . . . . . . . . . . . . 15
..^
..^
..^ |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . . 14
..^
..^
|
110 | 104, 109 | sylibr 224 |
. . . . . . . . . . . . 13
..^ |
111 | 16 | simp3d 1075 |
. . . . . . . . . . . . . 14
Disj
|
112 | 111 | ad4antr 768 |
. . . . . . . . . . . . 13
Disj |
113 | | nnct 12780 |
. . . . . . . . . . . . . . 15
|
114 | | mptct 9360 |
. . . . . . . . . . . . . . 15
..^ |
115 | 113, 114 | ax-mp 5 |
. . . . . . . . . . . . . 14
..^ |
116 | | rnct 9347 |
. . . . . . . . . . . . . 14
..^
..^ |
117 | 115, 116 | mp1i 13 |
. . . . . . . . . . . . 13
..^ |
118 | 43 | iundisj2 23317 |
. . . . . . . . . . . . . 14
Disj
..^ |
119 | | disjrnmpt 29398 |
. . . . . . . . . . . . . 14
Disj
..^
Disj
..^ |
120 | 118, 119 | mp1i 13 |
. . . . . . . . . . . . 13
Disj ..^ |
121 | | breq1 4656 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
122 | | disjeq1 4627 |
. . . . . . . . . . . . . . . . . 18
..^ Disj
Disj
..^ |
123 | 121, 122 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
..^ Disj
..^ Disj ..^ |
124 | | unieq 4444 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
125 | 124 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
126 | 123, 125 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
..^ Disj
..^
Disj
..^ ..^ |
127 | 126 | rspcv 3305 |
. . . . . . . . . . . . . . 15
..^
Disj
..^
Disj
..^ ..^ |
128 | 127 | imp 445 |
. . . . . . . . . . . . . 14
..^
Disj
..^ Disj ..^ ..^ |
129 | 128 | imp 445 |
. . . . . . . . . . . . 13
..^
Disj
..^
Disj
..^
..^ |
130 | 110, 112,
117, 120, 129 | syl22anc 1327 |
. . . . . . . . . . . 12
..^ |
131 | 56, 130 | syl5eqel 2705 |
. . . . . . . . . . 11
..^ |
132 | 52, 131 | eqeltrrd 2702 |
. . . . . . . . . 10
|
133 | 42, 132 | exlimddv 1863 |
. . . . . . . . 9
|
134 | 31, 133 | pm2.61dane 2881 |
. . . . . . . 8
|
135 | 134 | ex 450 |
. . . . . . 7
|
136 | 135 | ralrimiva 2966 |
. . . . . 6
|
137 | 25, 17, 136 | 3jca 1242 |
. . . . 5
|
138 | 11, 137 | jca 554 |
. . . 4
|
139 | | vex 3203 |
. . . . 5
|
140 | | issiga 30174 |
. . . . 5
sigAlgebra
|
141 | 139, 140 | ax-mp 5 |
. . . 4
sigAlgebra
|
142 | 138, 141 | sylibr 224 |
. . 3
sigAlgebra |
143 | 142 | ssriv 3607 |
. 2
sigAlgebra |
144 | 5, 143 | eqssi 3619 |
1
sigAlgebra |