Step | Hyp | Ref
| Expression |
1 | | issmfgt.s |
. . . . . . 7
SAlg |
2 | 1 | adantr 481 |
. . . . . 6
SMblFn SAlg |
3 | | simpr 477 |
. . . . . 6
SMblFn SMblFn |
4 | | issmfgt.d |
. . . . . 6
|
5 | 2, 3, 4 | smfdmss 40942 |
. . . . 5
SMblFn |
6 | 2, 3, 4 | smff 40941 |
. . . . 5
SMblFn |
7 | | nfv 1843 |
. . . . . . 7
|
8 | | nfv 1843 |
. . . . . . 7
SMblFn |
9 | 7, 8 | nfan 1828 |
. . . . . 6
SMblFn |
10 | 2, 5 | restuni4 39304 |
. . . . . . . . . . 11
SMblFn ↾t |
11 | 10 | eqcomd 2628 |
. . . . . . . . . 10
SMblFn
↾t |
12 | 11 | rabeqd 39276 |
. . . . . . . . 9
SMblFn ↾t |
13 | 12 | adantr 481 |
. . . . . . . 8
SMblFn
↾t |
14 | | nfv 1843 |
. . . . . . . . . . 11
|
15 | | nfv 1843 |
. . . . . . . . . . 11
SMblFn |
16 | 14, 15 | nfan 1828 |
. . . . . . . . . 10
SMblFn |
17 | | nfv 1843 |
. . . . . . . . . 10
|
18 | 16, 17 | nfan 1828 |
. . . . . . . . 9
SMblFn |
19 | | nfv 1843 |
. . . . . . . . 9
SMblFn |
20 | 1 | uniexd 39281 |
. . . . . . . . . . . . . 14
|
21 | 20 | adantr 481 |
. . . . . . . . . . . . 13
|
22 | | simpr 477 |
. . . . . . . . . . . . 13
|
23 | 21, 22 | ssexd 4805 |
. . . . . . . . . . . 12
|
24 | 5, 23 | syldan 487 |
. . . . . . . . . . 11
SMblFn |
25 | | eqid 2622 |
. . . . . . . . . . 11
↾t ↾t |
26 | 2, 24, 25 | subsalsal 40577 |
. . . . . . . . . 10
SMblFn ↾t SAlg |
27 | 26 | adantr 481 |
. . . . . . . . 9
SMblFn
↾t SAlg |
28 | | eqid 2622 |
. . . . . . . . 9
↾t
↾t |
29 | 6 | adantr 481 |
. . . . . . . . . . . 12
SMblFn
↾t |
30 | | simpr 477 |
. . . . . . . . . . . . 13
SMblFn
↾t ↾t |
31 | 10 | adantr 481 |
. . . . . . . . . . . . 13
SMblFn
↾t
↾t |
32 | 30, 31 | eleqtrd 2703 |
. . . . . . . . . . . 12
SMblFn
↾t |
33 | 29, 32 | ffvelrnd 6360 |
. . . . . . . . . . 11
SMblFn
↾t |
34 | 33 | rexrd 10089 |
. . . . . . . . . 10
SMblFn
↾t |
35 | 34 | adantlr 751 |
. . . . . . . . 9
SMblFn ↾t
|
36 | 2, 4 | issmfle 40954 |
. . . . . . . . . . . . . . 15
SMblFn SMblFn
↾t |
37 | 3, 36 | mpbid 222 |
. . . . . . . . . . . . . 14
SMblFn ↾t |
38 | 37 | simp3d 1075 |
. . . . . . . . . . . . 13
SMblFn
↾t |
39 | 10 | rabeqd 39276 |
. . . . . . . . . . . . . . 15
SMblFn ↾t
|
40 | 39 | eleq1d 2686 |
. . . . . . . . . . . . . 14
SMblFn ↾t ↾t
↾t |
41 | 40 | ralbidv 2986 |
. . . . . . . . . . . . 13
SMblFn ↾t
↾t
↾t |
42 | 38, 41 | mpbird 247 |
. . . . . . . . . . . 12
SMblFn ↾t
↾t |
43 | 42 | adantr 481 |
. . . . . . . . . . 11
SMblFn
↾t
↾t |
44 | | simpr 477 |
. . . . . . . . . . 11
SMblFn
|
45 | | rspa 2930 |
. . . . . . . . . . 11
↾t
↾t ↾t ↾t |
46 | 43, 44, 45 | syl2anc 693 |
. . . . . . . . . 10
SMblFn
↾t ↾t |
47 | 46 | adantlr 751 |
. . . . . . . . 9
SMblFn ↾t ↾t |
48 | | simpr 477 |
. . . . . . . . 9
SMblFn
|
49 | 18, 19, 27, 28, 35, 47, 48 | salpreimalegt 40920 |
. . . . . . . 8
SMblFn
↾t ↾t |
50 | 13, 49 | eqeltrd 2701 |
. . . . . . 7
SMblFn
↾t |
51 | 50 | ex 450 |
. . . . . 6
SMblFn
↾t |
52 | 9, 51 | ralrimi 2957 |
. . . . 5
SMblFn
↾t |
53 | 5, 6, 52 | 3jca 1242 |
. . . 4
SMblFn ↾t |
54 | 53 | ex 450 |
. . 3
SMblFn
↾t |
55 | | nfv 1843 |
. . . . . . 7
|
56 | | nfv 1843 |
. . . . . . 7
|
57 | | nfcv 2764 |
. . . . . . . 8
|
58 | | nfrab1 3122 |
. . . . . . . . 9
|
59 | | nfcv 2764 |
. . . . . . . . 9
↾t |
60 | 58, 59 | nfel 2777 |
. . . . . . . 8
↾t |
61 | 57, 60 | nfral 2945 |
. . . . . . 7
↾t |
62 | 55, 56, 61 | nf3an 1831 |
. . . . . 6
↾t |
63 | 14, 62 | nfan 1828 |
. . . . 5
↾t |
64 | | nfv 1843 |
. . . . . . 7
|
65 | | nfv 1843 |
. . . . . . 7
|
66 | | nfra1 2941 |
. . . . . . 7
↾t |
67 | 64, 65, 66 | nf3an 1831 |
. . . . . 6
↾t |
68 | 7, 67 | nfan 1828 |
. . . . 5
↾t |
69 | 1 | adantr 481 |
. . . . 5
↾t SAlg |
70 | | simpr1 1067 |
. . . . 5
↾t |
71 | | simpr2 1068 |
. . . . 5
↾t |
72 | | simpr3 1069 |
. . . . 5
↾t
↾t |
73 | 63, 68, 69, 4, 70, 71, 72 | issmfgtlem 40964 |
. . . 4
↾t SMblFn |
74 | 73 | ex 450 |
. . 3
↾t
SMblFn |
75 | 54, 74 | impbid 202 |
. 2
SMblFn
↾t |
76 | | breq1 4656 |
. . . . . . . 8
|
77 | 76 | rabbidv 3189 |
. . . . . . 7
|
78 | | fveq2 6191 |
. . . . . . . . . 10
|
79 | 78 | breq2d 4665 |
. . . . . . . . 9
|
80 | 79 | cbvrabv 3199 |
. . . . . . . 8
|
81 | 80 | a1i 11 |
. . . . . . 7
|
82 | 77, 81 | eqtrd 2656 |
. . . . . 6
|
83 | 82 | eleq1d 2686 |
. . . . 5
↾t
↾t |
84 | 83 | cbvralv 3171 |
. . . 4
↾t
↾t |
85 | 84 | 3anbi3i 1255 |
. . 3
↾t
↾t |
86 | 85 | a1i 11 |
. 2
↾t
↾t |
87 | 75, 86 | bitrd 268 |
1
SMblFn
↾t |