Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . 7
SMblFn SMblFn |
2 | | df-smblfn 40910 |
. . . . . . . . . 10
SMblFn SAlg
↾t |
3 | 2 | a1i 11 |
. . . . . . . . 9
SMblFn SAlg
↾t |
4 | | unieq 4444 |
. . . . . . . . . . . . 13
|
5 | 4 | oveq2d 6666 |
. . . . . . . . . . . 12
|
6 | 5 | rabeqd 39276 |
. . . . . . . . . . 11
↾t ↾t |
7 | | oveq1 6657 |
. . . . . . . . . . . . . 14
↾t
↾t |
8 | 7 | eleq2d 2687 |
. . . . . . . . . . . . 13
↾t
↾t |
9 | 8 | ralbidv 2986 |
. . . . . . . . . . . 12
↾t ↾t |
10 | 9 | rabbidv 3189 |
. . . . . . . . . . 11
↾t ↾t |
11 | 6, 10 | eqtrd 2656 |
. . . . . . . . . 10
↾t ↾t |
12 | 11 | adantl 482 |
. . . . . . . . 9
↾t ↾t |
13 | | issmflem.s |
. . . . . . . . 9
SAlg |
14 | | ovex 6678 |
. . . . . . . . . . 11
|
15 | 14 | rabex 4813 |
. . . . . . . . . 10
↾t |
16 | 15 | a1i 11 |
. . . . . . . . 9
↾t |
17 | 3, 12, 13, 16 | fvmptd 6288 |
. . . . . . . 8
SMblFn
↾t |
18 | 17 | adantr 481 |
. . . . . . 7
SMblFn SMblFn
↾t |
19 | 1, 18 | eleqtrd 2703 |
. . . . . 6
SMblFn ↾t |
20 | | elrabi 3359 |
. . . . . 6
↾t
|
21 | 19, 20 | syl 17 |
. . . . 5
SMblFn
|
22 | | issmflem.d |
. . . . . . 7
|
23 | | elpmi2 39418 |
. . . . . . 7
|
24 | 22, 23 | syl5eqss 3649 |
. . . . . 6
|
25 | 24 | adantl 482 |
. . . . 5
|
26 | 21, 25 | syldan 487 |
. . . 4
SMblFn |
27 | | elpmi 7876 |
. . . . . . 7
|
28 | 21, 27 | syl 17 |
. . . . . 6
SMblFn |
29 | 28 | simpld 475 |
. . . . 5
SMblFn |
30 | 22 | feq2i 6037 |
. . . . . 6
|
31 | 30 | a1i 11 |
. . . . 5
SMblFn |
32 | 29, 31 | mpbird 247 |
. . . 4
SMblFn |
33 | | cnveq 5296 |
. . . . . . . . . . . . . 14
|
34 | 33 | imaeq1d 5465 |
. . . . . . . . . . . . 13
|
35 | | dmeq 5324 |
. . . . . . . . . . . . . 14
|
36 | 35 | oveq2d 6666 |
. . . . . . . . . . . . 13
↾t ↾t |
37 | 34, 36 | eleq12d 2695 |
. . . . . . . . . . . 12
↾t
↾t |
38 | 37 | ralbidv 2986 |
. . . . . . . . . . 11
↾t
↾t |
39 | 38 | elrab 3363 |
. . . . . . . . . 10
↾t
↾t |
40 | 39 | simprbi 480 |
. . . . . . . . 9
↾t
↾t |
41 | 19, 40 | syl 17 |
. . . . . . . 8
SMblFn
↾t |
42 | 41 | adantr 481 |
. . . . . . 7
SMblFn
↾t |
43 | | simpr 477 |
. . . . . . 7
SMblFn
|
44 | | rspa 2930 |
. . . . . . 7
↾t
↾t |
45 | 42, 43, 44 | syl2anc 693 |
. . . . . 6
SMblFn
↾t |
46 | 32 | adantr 481 |
. . . . . . . 8
SMblFn
|
47 | | simpl 473 |
. . . . . . . . . 10
|
48 | | simpr 477 |
. . . . . . . . . . 11
|
49 | 48 | rexrd 10089 |
. . . . . . . . . 10
|
50 | 47, 49 | preimaioomnf 40929 |
. . . . . . . . 9
|
51 | 50 | eqcomd 2628 |
. . . . . . . 8
|
52 | 46, 43, 51 | syl2anc 693 |
. . . . . . 7
SMblFn
|
53 | 22 | oveq2i 6661 |
. . . . . . . 8
↾t ↾t |
54 | 53 | a1i 11 |
. . . . . . 7
SMblFn
↾t ↾t |
55 | 52, 54 | eleq12d 2695 |
. . . . . 6
SMblFn
↾t
↾t |
56 | 45, 55 | mpbird 247 |
. . . . 5
SMblFn
↾t |
57 | 56 | ralrimiva 2966 |
. . . 4
SMblFn
↾t |
58 | 26, 32, 57 | 3jca 1242 |
. . 3
SMblFn ↾t |
59 | 58 | ex 450 |
. 2
SMblFn
↾t |
60 | | reex 10027 |
. . . . . . . . 9
|
61 | 60 | a1i 11 |
. . . . . . . 8
|
62 | 13 | uniexd 39281 |
. . . . . . . . 9
|
63 | 62 | adantr 481 |
. . . . . . . 8
|
64 | | simprr 796 |
. . . . . . . 8
|
65 | | fssxp 6060 |
. . . . . . . . . . . 12
|
66 | 65 | adantl 482 |
. . . . . . . . . . 11
|
67 | | xpss1 5228 |
. . . . . . . . . . . 12
|
68 | 67 | adantr 481 |
. . . . . . . . . . 11
|
69 | 66, 68 | sstrd 3613 |
. . . . . . . . . 10
|
70 | 69 | adantl 482 |
. . . . . . . . 9
|
71 | | dmss 5323 |
. . . . . . . . . . . 12
|
72 | | dmxpss 5565 |
. . . . . . . . . . . . 13
|
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
|
74 | 71, 73 | sstrd 3613 |
. . . . . . . . . . 11
|
75 | 74 | adantl 482 |
. . . . . . . . . 10
|
76 | 22, 75 | syl5eqss 3649 |
. . . . . . . . 9
|
77 | 70, 76 | syldan 487 |
. . . . . . . 8
|
78 | | elpm2r 7875 |
. . . . . . . 8
|
79 | 61, 63, 64, 77, 78 | syl22anc 1327 |
. . . . . . 7
|
80 | 79 | 3adantr3 1222 |
. . . . . 6
↾t
|
81 | 22 | a1i 11 |
. . . . . . . . . . . . 13
|
82 | 81 | oveq2d 6666 |
. . . . . . . . . . . 12
↾t ↾t |
83 | 51, 82 | eleq12d 2695 |
. . . . . . . . . . 11
↾t
↾t |
84 | 83 | ralbidva 2985 |
. . . . . . . . . 10
↾t
↾t |
85 | 84 | biimpd 219 |
. . . . . . . . 9
↾t ↾t |
86 | 85 | imp 445 |
. . . . . . . 8
↾t
↾t |
87 | 86 | adantl 482 |
. . . . . . 7
↾t
↾t |
88 | 87 | 3adantr1 1220 |
. . . . . 6
↾t
↾t |
89 | 80, 88 | jca 554 |
. . . . 5
↾t
↾t |
90 | 89, 39 | sylibr 224 |
. . . 4
↾t ↾t |
91 | 17 | eqcomd 2628 |
. . . . 5
↾t SMblFn |
92 | 91 | adantr 481 |
. . . 4
↾t
↾t SMblFn |
93 | 90, 92 | eleqtrd 2703 |
. . 3
↾t SMblFn |
94 | 93 | ex 450 |
. 2
↾t
SMblFn |
95 | 59, 94 | impbid 202 |
1
SMblFn
↾t |