Proof of Theorem smfsupmpt
Step | Hyp | Ref
| Expression |
1 | | smfsupmpt.g |
. . . 4
|
2 | 1 | a1i 11 |
. . 3
|
3 | | smfsupmpt.x |
. . . . 5
|
4 | | smfsupmpt.d |
. . . . . . 7
|
5 | 4 | a1i 11 |
. . . . . 6
|
6 | | smfsupmpt.n |
. . . . . . . . 9
|
7 | | eqidd 2623 |
. . . . . . . . . . . 12
|
8 | | smfsupmpt.f |
. . . . . . . . . . . 12
SMblFn |
9 | 7, 8 | fvmpt2d 6293 |
. . . . . . . . . . 11
|
10 | 9 | dmeqd 5326 |
. . . . . . . . . 10
|
11 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
12 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
13 | 11, 12 | nfel 2777 |
. . . . . . . . . . . 12
|
14 | 3, 13 | nfan 1828 |
. . . . . . . . . . 11
|
15 | | eqid 2622 |
. . . . . . . . . . 11
|
16 | | smfsupmpt.s |
. . . . . . . . . . . . . 14
SAlg |
17 | 16 | adantr 481 |
. . . . . . . . . . . . 13
SAlg |
18 | | smfsupmpt.b |
. . . . . . . . . . . . . 14
|
19 | 18 | 3expa 1265 |
. . . . . . . . . . . . 13
|
20 | 14, 17, 19, 8 | smffmpt 41011 |
. . . . . . . . . . . 12
|
21 | 20 | fvmptelrn 39428 |
. . . . . . . . . . 11
|
22 | 14, 15, 21 | dmmptdf 39417 |
. . . . . . . . . 10
|
23 | | eqidd 2623 |
. . . . . . . . . 10
|
24 | 10, 22, 23 | 3eqtrrd 2661 |
. . . . . . . . 9
|
25 | 6, 24 | iineq2d 4541 |
. . . . . . . 8
|
26 | | nfcv 2764 |
. . . . . . . . 9
|
27 | | nfmpt1 4747 |
. . . . . . . . . . . . 13
|
28 | 12, 27 | nfmpt 4746 |
. . . . . . . . . . . 12
|
29 | 28, 11 | nffv 6198 |
. . . . . . . . . . 11
|
30 | 29 | nfdm 5367 |
. . . . . . . . . 10
|
31 | 12, 30 | nfiin 4549 |
. . . . . . . . 9
|
32 | 26, 31 | rabeqf 3190 |
. . . . . . . 8
|
33 | 25, 32 | syl 17 |
. . . . . . 7
|
34 | | smfsupmpt.y |
. . . . . . . . . 10
|
35 | | nfv 1843 |
. . . . . . . . . 10
|
36 | 34, 35 | nfan 1828 |
. . . . . . . . 9
|
37 | | nfcv 2764 |
. . . . . . . . . . . 12
|
38 | | nfii1 4551 |
. . . . . . . . . . . 12
|
39 | 37, 38 | nfel 2777 |
. . . . . . . . . . 11
|
40 | 6, 39 | nfan 1828 |
. . . . . . . . . 10
|
41 | | simpll 790 |
. . . . . . . . . . 11
|
42 | | simpr 477 |
. . . . . . . . . . 11
|
43 | | eliinid 39294 |
. . . . . . . . . . . . 13
|
44 | 43 | adantll 750 |
. . . . . . . . . . . 12
|
45 | 24 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
46 | 45 | adantlr 751 |
. . . . . . . . . . . 12
|
47 | 44, 46 | eleqtrd 2703 |
. . . . . . . . . . 11
|
48 | 9 | fveq1d 6193 |
. . . . . . . . . . . . . 14
|
49 | 48 | 3adant3 1081 |
. . . . . . . . . . . . 13
|
50 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
51 | 15 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
52 | 50, 18, 51 | syl2anc 693 |
. . . . . . . . . . . . 13
|
53 | 49, 52 | eqtr2d 2657 |
. . . . . . . . . . . 12
|
54 | 53 | breq1d 4663 |
. . . . . . . . . . 11
|
55 | 41, 42, 47, 54 | syl3anc 1326 |
. . . . . . . . . 10
|
56 | 40, 55 | ralbida 2982 |
. . . . . . . . 9
|
57 | 36, 56 | rexbid 3051 |
. . . . . . . 8
|
58 | 3, 57 | rabbida 39274 |
. . . . . . 7
|
59 | 33, 58 | eqtrd 2656 |
. . . . . 6
|
60 | 5, 59 | eqtrd 2656 |
. . . . 5
|
61 | 3, 60 | alrimi 2082 |
. . . 4
|
62 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
63 | | nfra1 2941 |
. . . . . . . . . . . . . 14
|
64 | 62, 63 | nfrex 3007 |
. . . . . . . . . . . . 13
|
65 | | nfii1 4551 |
. . . . . . . . . . . . 13
|
66 | 64, 65 | nfrab 3123 |
. . . . . . . . . . . 12
|
67 | 4, 66 | nfcxfr 2762 |
. . . . . . . . . . 11
|
68 | 37, 67 | nfel 2777 |
. . . . . . . . . 10
|
69 | 6, 68 | nfan 1828 |
. . . . . . . . 9
|
70 | | simpll 790 |
. . . . . . . . . 10
|
71 | | simpr 477 |
. . . . . . . . . 10
|
72 | 4 | eleq2i 2693 |
. . . . . . . . . . . . . . 15
|
73 | 72 | biimpi 206 |
. . . . . . . . . . . . . 14
|
74 | | rabidim1 3117 |
. . . . . . . . . . . . . 14
|
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . 13
|
76 | 75 | adantr 481 |
. . . . . . . . . . . 12
|
77 | | simpr 477 |
. . . . . . . . . . . 12
|
78 | | eliinid 39294 |
. . . . . . . . . . . 12
|
79 | 76, 77, 78 | syl2anc 693 |
. . . . . . . . . . 11
|
80 | 79 | adantll 750 |
. . . . . . . . . 10
|
81 | 53 | idi 2 |
. . . . . . . . . 10
|
82 | 70, 71, 80, 81 | syl3anc 1326 |
. . . . . . . . 9
|
83 | 69, 82 | mpteq2da 4743 |
. . . . . . . 8
|
84 | 83 | rneqd 5353 |
. . . . . . 7
|
85 | 84 | supeq1d 8352 |
. . . . . 6
|
86 | 85 | ex 450 |
. . . . 5
|
87 | 3, 86 | ralrimi 2957 |
. . . 4
|
88 | | mpteq12f 4731 |
. . . 4
|
89 | 61, 87, 88 | syl2anc 693 |
. . 3
|
90 | 2, 89 | eqtrd 2656 |
. 2
|
91 | | nfmpt1 4747 |
. . 3
|
92 | | smfsupmpt.m |
. . 3
|
93 | | smfsupmpt.z |
. . 3
|
94 | | eqid 2622 |
. . . 4
|
95 | 6, 8, 94 | fmptdf 6387 |
. . 3
SMblFn |
96 | | eqid 2622 |
. . 3
|
97 | | eqid 2622 |
. . 3
|
98 | 91, 28, 92, 93, 16, 95, 96, 97 | smfsup 41020 |
. 2
SMblFn |
99 | 90, 98 | eqeltrd 2701 |
1
SMblFn |