Step | Hyp | Ref
| Expression |
1 | | f1stres 7190 |
. . . 4
|
2 | | 1stmbfm.1 |
. . . . . 6
sigAlgebra |
3 | | 1stmbfm.2 |
. . . . . 6
sigAlgebra |
4 | | sxuni 30256 |
. . . . . 6
sigAlgebra
sigAlgebra
×s |
5 | 2, 3, 4 | syl2anc 693 |
. . . . 5
×s |
6 | 5 | feq2d 6031 |
. . . 4
×s |
7 | 1, 6 | mpbii 223 |
. . 3
×s |
8 | | unielsiga 30191 |
. . . . 5
sigAlgebra |
9 | 2, 8 | syl 17 |
. . . 4
|
10 | | sxsiga 30254 |
. . . . . 6
sigAlgebra
sigAlgebra
×s sigAlgebra |
11 | 2, 3, 10 | syl2anc 693 |
. . . . 5
×s sigAlgebra |
12 | | unielsiga 30191 |
. . . . 5
×s sigAlgebra ×s ×s |
13 | 11, 12 | syl 17 |
. . . 4
×s ×s |
14 | 9, 13 | elmapd 7871 |
. . 3
×s
×s |
15 | 7, 14 | mpbird 247 |
. 2
×s |
16 | | sgon 30187 |
. . . . . . . . . . 11
sigAlgebra sigAlgebra |
17 | | sigasspw 30179 |
. . . . . . . . . . 11
sigAlgebra |
18 | | pwssb 4612 |
. . . . . . . . . . . 12
|
19 | 18 | biimpi 206 |
. . . . . . . . . . 11
|
20 | 2, 16, 17, 19 | 4syl 19 |
. . . . . . . . . 10
|
21 | 20 | r19.21bi 2932 |
. . . . . . . . 9
|
22 | | xpss1 5228 |
. . . . . . . . 9
|
23 | 21, 22 | syl 17 |
. . . . . . . 8
|
24 | 23 | sseld 3602 |
. . . . . . 7
|
25 | 24 | pm4.71rd 667 |
. . . . . 6
|
26 | | ffn 6045 |
. . . . . . . 8
|
27 | | elpreima 6337 |
. . . . . . . 8
|
28 | 1, 26, 27 | mp2b 10 |
. . . . . . 7
|
29 | | fvres 6207 |
. . . . . . . . . 10
|
30 | 29 | eleq1d 2686 |
. . . . . . . . 9
|
31 | | 1st2nd2 7205 |
. . . . . . . . . 10
|
32 | | xp2nd 7199 |
. . . . . . . . . 10
|
33 | | elxp6 7200 |
. . . . . . . . . . . 12
|
34 | | anass 681 |
. . . . . . . . . . . 12
|
35 | | an32 839 |
. . . . . . . . . . . 12
|
36 | 33, 34, 35 | 3bitr2i 288 |
. . . . . . . . . . 11
|
37 | 36 | baib 944 |
. . . . . . . . . 10
|
38 | 31, 32, 37 | syl2anc 693 |
. . . . . . . . 9
|
39 | 30, 38 | bitr4d 271 |
. . . . . . . 8
|
40 | 39 | pm5.32i 669 |
. . . . . . 7
|
41 | 28, 40 | bitri 264 |
. . . . . 6
|
42 | 25, 41 | syl6rbbr 279 |
. . . . 5
|
43 | 42 | eqrdv 2620 |
. . . 4
|
44 | 2 | adantr 481 |
. . . . 5
sigAlgebra |
45 | 3 | adantr 481 |
. . . . 5
sigAlgebra |
46 | | simpr 477 |
. . . . 5
|
47 | | eqid 2622 |
. . . . . . . 8
|
48 | | issgon 30186 |
. . . . . . . 8
sigAlgebra sigAlgebra |
49 | 3, 47, 48 | sylanblrc 697 |
. . . . . . 7
sigAlgebra |
50 | | baselsiga 30178 |
. . . . . . 7
sigAlgebra |
51 | 49, 50 | syl 17 |
. . . . . 6
|
52 | 51 | adantr 481 |
. . . . 5
|
53 | | elsx 30257 |
. . . . 5
sigAlgebra
sigAlgebra ×s |
54 | 44, 45, 46, 52, 53 | syl22anc 1327 |
. . . 4
×s |
55 | 43, 54 | eqeltrd 2701 |
. . 3
×s |
56 | 55 | ralrimiva 2966 |
. 2
×s |
57 | 11, 2 | ismbfm 30314 |
. 2
×s MblFnM
×s
×s |
58 | 15, 56, 57 | mpbir2and 957 |
1
×s MblFnM |