Step | Hyp | Ref
| Expression |
1 | | imambfm.2 |
. . . . 5
sigAlgebra |
2 | 1 | adantr 481 |
. . . 4
MblFnM sigAlgebra |
3 | | imambfm.3 |
. . . . . 6
sigaGen |
4 | | imambfm.1 |
. . . . . . 7
|
5 | 4 | sgsiga 30205 |
. . . . . 6
sigaGen
sigAlgebra |
6 | 3, 5 | eqeltrd 2701 |
. . . . 5
sigAlgebra |
7 | 6 | adantr 481 |
. . . 4
MblFnM sigAlgebra |
8 | | simpr 477 |
. . . 4
MblFnM MblFnM |
9 | 2, 7, 8 | mbfmf 30317 |
. . 3
MblFnM |
10 | 1 | ad2antrr 762 |
. . . . 5
MblFnM
sigAlgebra |
11 | 6 | ad2antrr 762 |
. . . . 5
MblFnM
sigAlgebra |
12 | | simplr 792 |
. . . . 5
MblFnM MblFnM |
13 | | sssigagen 30208 |
. . . . . . . . 9
sigaGen |
14 | 4, 13 | syl 17 |
. . . . . . . 8
sigaGen |
15 | 14, 3 | sseqtr4d 3642 |
. . . . . . 7
|
16 | 15 | ad2antrr 762 |
. . . . . 6
MblFnM |
17 | | simpr 477 |
. . . . . 6
MblFnM |
18 | 16, 17 | sseldd 3604 |
. . . . 5
MblFnM |
19 | 10, 11, 12, 18 | mbfmcnvima 30319 |
. . . 4
MblFnM |
20 | 19 | ralrimiva 2966 |
. . 3
MblFnM |
21 | 9, 20 | jca 554 |
. 2
MblFnM
|
22 | | unielsiga 30191 |
. . . . . 6
sigAlgebra |
23 | 6, 22 | syl 17 |
. . . . 5
|
24 | 23 | adantr 481 |
. . . 4
|
25 | | unielsiga 30191 |
. . . . . 6
sigAlgebra |
26 | 1, 25 | syl 17 |
. . . . 5
|
27 | 26 | adantr 481 |
. . . 4
|
28 | | simprl 794 |
. . . 4
|
29 | | elmapg 7870 |
. . . . 5
|
30 | 29 | biimpar 502 |
. . . 4
|
31 | 24, 27, 28, 30 | syl21anc 1325 |
. . 3
|
32 | 3 | adantr 481 |
. . . . . 6
sigaGen |
33 | | simpl 473 |
. . . . . . . . 9
|
34 | | ssrab2 3687 |
. . . . . . . . . . 11
|
35 | | pwuni 4474 |
. . . . . . . . . . 11
|
36 | 34, 35 | sstri 3612 |
. . . . . . . . . 10
|
37 | 36 | a1i 11 |
. . . . . . . . 9
|
38 | | fimacnv 6347 |
. . . . . . . . . . . . 13
|
39 | 38 | ad2antrl 764 |
. . . . . . . . . . . 12
|
40 | 39, 27 | eqeltrd 2701 |
. . . . . . . . . . 11
|
41 | | imaeq2 5462 |
. . . . . . . . . . . . 13
|
42 | 41 | eleq1d 2686 |
. . . . . . . . . . . 12
|
43 | 42 | elrab 3363 |
. . . . . . . . . . 11
|
44 | 24, 40, 43 | sylanbrc 698 |
. . . . . . . . . 10
|
45 | 6 | ad2antrr 762 |
. . . . . . . . . . . . 13
sigAlgebra |
46 | 45, 22 | syl 17 |
. . . . . . . . . . . . 13
|
47 | | elrabi 3359 |
. . . . . . . . . . . . . 14
|
48 | 47 | adantl 482 |
. . . . . . . . . . . . 13
|
49 | | difelsiga 30196 |
. . . . . . . . . . . . 13
sigAlgebra
|
50 | 45, 46, 48, 49 | syl3anc 1326 |
. . . . . . . . . . . 12
|
51 | | simplrl 800 |
. . . . . . . . . . . . . 14
|
52 | | ffun 6048 |
. . . . . . . . . . . . . 14
|
53 | | difpreima 6343 |
. . . . . . . . . . . . . 14
|
54 | 51, 52, 53 | 3syl 18 |
. . . . . . . . . . . . 13
|
55 | 39 | difeq1d 3727 |
. . . . . . . . . . . . . . 15
|
56 | 55 | adantr 481 |
. . . . . . . . . . . . . 14
|
57 | 1 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
sigAlgebra |
58 | 57, 25 | syl 17 |
. . . . . . . . . . . . . . 15
|
59 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . . . 19
|
60 | 59 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
|
61 | 60 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
|
62 | 61 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
63 | 62 | adantl 482 |
. . . . . . . . . . . . . . 15
|
64 | | difelsiga 30196 |
. . . . . . . . . . . . . . 15
sigAlgebra |
65 | 57, 58, 63, 64 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
66 | 56, 65 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
67 | 54, 66 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
68 | | imaeq2 5462 |
. . . . . . . . . . . . . 14
|
69 | 68 | eleq1d 2686 |
. . . . . . . . . . . . 13
|
70 | 69 | elrab 3363 |
. . . . . . . . . . . 12
|
71 | 50, 67, 70 | sylanbrc 698 |
. . . . . . . . . . 11
|
72 | 71 | ralrimiva 2966 |
. . . . . . . . . 10
|
73 | 6 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
sigAlgebra |
74 | | sspwb 4917 |
. . . . . . . . . . . . . . . . 17
|
75 | 34, 74 | mpbi 220 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | sseli 3599 |
. . . . . . . . . . . . . . 15
|
77 | 76 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
78 | | simpr 477 |
. . . . . . . . . . . . . 14
|
79 | | sigaclcu 30180 |
. . . . . . . . . . . . . 14
sigAlgebra
|
80 | 73, 77, 78, 79 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
81 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
|
82 | 81 | simpld 475 |
. . . . . . . . . . . . . . 15
|
83 | | unipreima 29446 |
. . . . . . . . . . . . . . 15
|
84 | 82, 52, 83 | 3syl 18 |
. . . . . . . . . . . . . 14
|
85 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
sigAlgebra |
86 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
87 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
|
88 | | elelpwi 4171 |
. . . . . . . . . . . . . . . . . 18
|
89 | 86, 87, 88 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
90 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . . . . 20
|
91 | 90 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
92 | 91 | elrab 3363 |
. . . . . . . . . . . . . . . . . 18
|
93 | 92 | simprbi 480 |
. . . . . . . . . . . . . . . . 17
|
94 | 89, 93 | syl 17 |
. . . . . . . . . . . . . . . 16
|
95 | 94 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
|
96 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
97 | 96 | sigaclcuni 30181 |
. . . . . . . . . . . . . . 15
sigAlgebra
|
98 | 85, 95, 78, 97 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
99 | 84, 98 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
100 | | imaeq2 5462 |
. . . . . . . . . . . . . . 15
|
101 | 100 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
102 | 101 | elrab 3363 |
. . . . . . . . . . . . 13
|
103 | 80, 99, 102 | sylanbrc 698 |
. . . . . . . . . . . 12
|
104 | 103 | ex 450 |
. . . . . . . . . . 11
|
105 | 104 | ralrimiva 2966 |
. . . . . . . . . 10
|
106 | 44, 72, 105 | 3jca 1242 |
. . . . . . . . 9
|
107 | | rabexg 4812 |
. . . . . . . . . . 11
sigAlgebra |
108 | | issiga 30174 |
. . . . . . . . . . 11
sigAlgebra
|
109 | 6, 107, 108 | 3syl 18 |
. . . . . . . . . 10
sigAlgebra
|
110 | 109 | biimpar 502 |
. . . . . . . . 9
sigAlgebra |
111 | 33, 37, 106, 110 | syl12anc 1324 |
. . . . . . . 8
sigAlgebra |
112 | 3 | unieqd 4446 |
. . . . . . . . . . . 12
sigaGen |
113 | | unisg 30206 |
. . . . . . . . . . . . 13
sigaGen |
114 | 4, 113 | syl 17 |
. . . . . . . . . . . 12
sigaGen |
115 | 112, 114 | eqtrd 2656 |
. . . . . . . . . . 11
|
116 | 115 | fveq2d 6195 |
. . . . . . . . . 10
sigAlgebra sigAlgebra |
117 | 116 | eleq2d 2687 |
. . . . . . . . 9
sigAlgebra
sigAlgebra |
118 | 117 | adantr 481 |
. . . . . . . 8
sigAlgebra
sigAlgebra |
119 | 111, 118 | mpbid 222 |
. . . . . . 7
sigAlgebra |
120 | 15 | adantr 481 |
. . . . . . . 8
|
121 | | simprr 796 |
. . . . . . . 8
|
122 | | ssrab 3680 |
. . . . . . . 8
|
123 | 120, 121,
122 | sylanbrc 698 |
. . . . . . 7
|
124 | | sigagenss 30212 |
. . . . . . 7
sigAlgebra sigaGen |
125 | 119, 123,
124 | syl2anc 693 |
. . . . . 6
sigaGen |
126 | 32, 125 | eqsstrd 3639 |
. . . . 5
|
127 | 34 | a1i 11 |
. . . . 5
|
128 | 126, 127 | eqssd 3620 |
. . . 4
|
129 | | rabid2 3118 |
. . . 4
|
130 | 128, 129 | sylib 208 |
. . 3
|
131 | 1 | adantr 481 |
. . . 4
sigAlgebra |
132 | 6 | adantr 481 |
. . . 4
sigAlgebra |
133 | 131, 132 | ismbfm 30314 |
. . 3
MblFnM
|
134 | 31, 130, 133 | mpbir2and 957 |
. 2
MblFnM |
135 | 21, 134 | impbida 877 |
1
MblFnM
|