Step | Hyp | Ref
| Expression |
1 | | f2ndres 7191 |
. . . 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 | 3, 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 | 3, 16, 17, 19 | 4syl 19 |
. . . . . . . . . 10
|
21 | 20 | r19.21bi 2932 |
. . . . . . . . 9
|
22 | | xpss2 5229 |
. . . . . . . . 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 | | xp1st 7198 |
. . . . . . . . . 10
|
33 | | elxp6 7200 |
. . . . . . . . . . . 12
|
34 | | anass 681 |
. . . . . . . . . . . 12
|
35 | 33, 34 | bitr4i 267 |
. . . . . . . . . . 11
|
36 | 35 | baib 944 |
. . . . . . . . . 10
|
37 | 31, 32, 36 | syl2anc 693 |
. . . . . . . . 9
|
38 | 30, 37 | bitr4d 271 |
. . . . . . . 8
|
39 | 38 | pm5.32i 669 |
. . . . . . 7
|
40 | 28, 39 | bitri 264 |
. . . . . 6
|
41 | 25, 40 | syl6rbbr 279 |
. . . . 5
|
42 | 41 | eqrdv 2620 |
. . . 4
|
43 | 2 | adantr 481 |
. . . . 5
sigAlgebra |
44 | 3 | adantr 481 |
. . . . 5
sigAlgebra |
45 | | eqid 2622 |
. . . . . . . 8
|
46 | | issgon 30186 |
. . . . . . . 8
sigAlgebra sigAlgebra |
47 | 2, 45, 46 | sylanblrc 697 |
. . . . . . 7
sigAlgebra |
48 | | baselsiga 30178 |
. . . . . . 7
sigAlgebra |
49 | 47, 48 | syl 17 |
. . . . . 6
|
50 | 49 | adantr 481 |
. . . . 5
|
51 | | simpr 477 |
. . . . 5
|
52 | | elsx 30257 |
. . . . 5
sigAlgebra
sigAlgebra
×s |
53 | 43, 44, 50, 51, 52 | syl22anc 1327 |
. . . 4
×s |
54 | 42, 53 | eqeltrd 2701 |
. . 3
×s |
55 | 54 | ralrimiva 2966 |
. 2
×s |
56 | 11, 3 | ismbfm 30314 |
. 2
×s MblFnM
×s
×s |
57 | 15, 55, 56 | mpbir2and 957 |
1
×s MblFnM |