Step | Hyp | Ref
| Expression |
1 | | simp3 994 |
. . . . . . . . . . . . . . . . . 18
DECID
|
2 | | fof 5418 |
. . . . . . . . . . . . . . . . . 18
|
3 | 1, 2 | syl 14 |
. . . . . . . . . . . . . . . . 17
DECID
|
4 | 3 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
DECID
|
5 | | simpr 109 |
. . . . . . . . . . . . . . . 16
DECID
|
6 | 4, 5 | ffvelrnd 5629 |
. . . . . . . . . . . . . . 15
DECID
|
7 | 3 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
DECID |
8 | | simpllr 529 |
. . . . . . . . . . . . . . . 16
DECID |
9 | 7, 8 | ffvelrnd 5629 |
. . . . . . . . . . . . . . 15
DECID |
10 | | elequ1 2145 |
. . . . . . . . . . . . . . . . 17
|
11 | 10 | dcbid 833 |
. . . . . . . . . . . . . . . 16
DECID
DECID
|
12 | | simpll2 1032 |
. . . . . . . . . . . . . . . 16
DECID
DECID |
13 | | simpr 109 |
. . . . . . . . . . . . . . . 16
DECID
|
14 | 11, 12, 13 | rspcdva 2839 |
. . . . . . . . . . . . . . 15
DECID
DECID |
15 | 6, 9, 14 | ifcldadc 3554 |
. . . . . . . . . . . . . 14
DECID
|
16 | 15 | fmpttd 5648 |
. . . . . . . . . . . . 13
DECID
|
17 | 16 | ffnd 5346 |
. . . . . . . . . . . 12
DECID
|
18 | | fvelrnb 5542 |
. . . . . . . . . . . . . . 15
|
19 | 17, 18 | syl 14 |
. . . . . . . . . . . . . 14
DECID
|
20 | 1 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . 18
DECID
|
21 | | foelrn 5729 |
. . . . . . . . . . . . . . . . . 18
|
22 | 20, 21 | sylancom 418 |
. . . . . . . . . . . . . . . . 17
DECID
|
23 | | simpll1 1031 |
. . . . . . . . . . . . . . . . . 18
DECID
|
24 | | eqid 2170 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
25 | | elequ1 2145 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
26 | | fveq2 5494 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
27 | 25, 26 | ifbieq1d 3547 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
28 | 23 | sselda 3147 |
. . . . . . . . . . . . . . . . . . . . . . . 24
DECID
|
29 | 3 | ad4antr 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
DECID
|
30 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
DECID
|
31 | 29, 30 | ffvelrnd 5629 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
DECID
|
32 | 3 | ffvelrnda 5628 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
DECID
|
33 | 32 | ad3antrrr 489 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
DECID
|
34 | | elequ1 2145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
35 | 34 | dcbid 833 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
DECID
DECID
|
36 | | simp2 993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
DECID
DECID |
37 | 36 | ad3antrrr 489 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
DECID
DECID |
38 | 35, 37, 28 | rspcdva 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
DECID
DECID
|
39 | 31, 33, 38 | ifcldadc 3554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
DECID
|
40 | 24, 27, 28, 39 | fvmptd3 5587 |
. . . . . . . . . . . . . . . . . . . . . . 23
DECID
|
41 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . . . . . 24
DECID
|
42 | 41 | iftrued 3532 |
. . . . . . . . . . . . . . . . . . . . . . 23
DECID
|
43 | 40, 42 | eqtrd 2203 |
. . . . . . . . . . . . . . . . . . . . . 22
DECID
|
44 | 43 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . 21
DECID
|
45 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . . 21
DECID
|
46 | 44, 45 | eqtr4d 2206 |
. . . . . . . . . . . . . . . . . . . 20
DECID
|
47 | 46 | ex 114 |
. . . . . . . . . . . . . . . . . . 19
DECID
|
48 | 47 | reximdva 2572 |
. . . . . . . . . . . . . . . . . 18
DECID
|
49 | | ssrexv 3212 |
. . . . . . . . . . . . . . . . . 18
|
50 | 23, 48, 49 | sylsyld 58 |
. . . . . . . . . . . . . . . . 17
DECID
|
51 | 22, 50 | mpd 13 |
. . . . . . . . . . . . . . . 16
DECID
|
52 | 51 | ex 114 |
. . . . . . . . . . . . . . 15
DECID
|
53 | | simpr 109 |
. . . . . . . . . . . . . . . . 17
DECID |
54 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . 20
DECID
|
55 | 3 | ad3antrrr 489 |
. . . . . . . . . . . . . . . . . . . . . 22
DECID
|
56 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . . . 22
DECID
|
57 | 55, 56 | ffvelrnd 5629 |
. . . . . . . . . . . . . . . . . . . . 21
DECID
|
58 | 32 | ad2antrr 485 |
. . . . . . . . . . . . . . . . . . . . 21
DECID |
59 | | simpll2 1032 |
. . . . . . . . . . . . . . . . . . . . . 22
DECID
DECID |
60 | 35, 59, 54 | rspcdva 2839 |
. . . . . . . . . . . . . . . . . . . . 21
DECID
DECID |
61 | 57, 58, 60 | ifcldadc 3554 |
. . . . . . . . . . . . . . . . . . . 20
DECID
|
62 | 24, 27, 54, 61 | fvmptd3 5587 |
. . . . . . . . . . . . . . . . . . 19
DECID
|
63 | 62, 61 | eqeltrd 2247 |
. . . . . . . . . . . . . . . . . 18
DECID
|
64 | 63 | adantr 274 |
. . . . . . . . . . . . . . . . 17
DECID |
65 | 53, 64 | eqeltrrd 2248 |
. . . . . . . . . . . . . . . 16
DECID |
66 | 65 | rexlimdva2 2590 |
. . . . . . . . . . . . . . 15
DECID
|
67 | 52, 66 | impbid 128 |
. . . . . . . . . . . . . 14
DECID
|
68 | 19, 67 | bitr4d 190 |
. . . . . . . . . . . . 13
DECID
|
69 | 68 | eqrdv 2168 |
. . . . . . . . . . . 12
DECID
|
70 | | df-fo 5202 |
. . . . . . . . . . . 12
|
71 | 17, 69, 70 | sylanbrc 415 |
. . . . . . . . . . 11
DECID
|
72 | | omex 4575 |
. . . . . . . . . . . . 13
|
73 | 72 | mptex 5719 |
. . . . . . . . . . . 12
|
74 | | foeq1 5414 |
. . . . . . . . . . . 12
|
75 | 73, 74 | spcev 2825 |
. . . . . . . . . . 11
|
76 | 71, 75 | syl 14 |
. . . . . . . . . 10
DECID
|
77 | | elex2 2746 |
. . . . . . . . . . . 12
|
78 | 32, 77 | syl 14 |
. . . . . . . . . . 11
DECID
|
79 | | ctm 7082 |
. . . . . . . . . . 11
⊔
|
80 | 78, 79 | syl 14 |
. . . . . . . . . 10
DECID
⊔
|
81 | 76, 80 | mpbird 166 |
. . . . . . . . 9
DECID
⊔ |
82 | | simpl1 995 |
. . . . . . . . . 10
DECID
|
83 | 36 | adantr 274 |
. . . . . . . . . 10
DECID
DECID |
84 | 1 | adantr 274 |
. . . . . . . . . 10
DECID
|
85 | | simpr 109 |
. . . . . . . . . 10
DECID
|
86 | 82, 83, 84, 85 | ctssdclemn0 7083 |
. . . . . . . . 9
DECID
⊔ |
87 | | eleq1 2233 |
. . . . . . . . . . . 12
|
88 | 87 | dcbid 833 |
. . . . . . . . . . 11
DECID DECID |
89 | | peano1 4576 |
. . . . . . . . . . . 12
|
90 | 89 | a1i 9 |
. . . . . . . . . . 11
DECID
|
91 | 88, 36, 90 | rspcdva 2839 |
. . . . . . . . . 10
DECID
DECID |
92 | | exmiddc 831 |
. . . . . . . . . 10
DECID |
93 | 91, 92 | syl 14 |
. . . . . . . . 9
DECID
|
94 | 81, 86, 93 | mpjaodan 793 |
. . . . . . . 8
DECID
⊔ |
95 | 94 | 3expia 1200 |
. . . . . . 7
DECID
⊔ |
96 | 95 | exlimdv 1812 |
. . . . . 6
DECID
⊔ |
97 | 96 | 3impia 1195 |
. . . . 5
DECID
⊔ |
98 | 97 | 3com23 1204 |
. . . 4
DECID ⊔ |
99 | 98 | exlimiv 1591 |
. . 3
DECID ⊔ |
100 | | foeq1 5414 |
. . . 4
⊔
⊔ |
101 | 100 | cbvexv 1911 |
. . 3
⊔
⊔
|
102 | 99, 101 | sylib 121 |
. 2
DECID ⊔ |
103 | | ctssdclemr 7085 |
. 2
⊔
DECID |
104 | 102, 103 | impbii 125 |
1
DECID
⊔ |