Step | Hyp | Ref
| Expression |
1 | | brdomi 6739 |
. . . . 5
|
2 | 1 | ad2antll 491 |
. . . 4
EXMID
|
3 | | df-f1 5213 |
. . . . . . . . . . . . . . . . 17
|
4 | 3 | simprbi 275 |
. . . . . . . . . . . . . . . 16
|
5 | | vex 2738 |
. . . . . . . . . . . . . . . . . 18
|
6 | 5 | fconst 5403 |
. . . . . . . . . . . . . . . . 17
|
7 | | ffun 5360 |
. . . . . . . . . . . . . . . . 17
|
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
9 | 4, 8 | jctir 313 |
. . . . . . . . . . . . . . 15
|
10 | | df-rn 4631 |
. . . . . . . . . . . . . . . . . 18
|
11 | 10 | eqcomi 2179 |
. . . . . . . . . . . . . . . . 17
|
12 | 5 | snm 3709 |
. . . . . . . . . . . . . . . . . 18
|
13 | | dmxpm 4840 |
. . . . . . . . . . . . . . . . . 18
|
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
15 | 11, 14 | ineq12i 3332 |
. . . . . . . . . . . . . . . 16
|
16 | | disjdif 3493 |
. . . . . . . . . . . . . . . 16
|
17 | 15, 16 | eqtri 2196 |
. . . . . . . . . . . . . . 15
|
18 | | funun 5252 |
. . . . . . . . . . . . . . 15
|
19 | 9, 17, 18 | sylancl 413 |
. . . . . . . . . . . . . 14
|
20 | 19 | adantl 277 |
. . . . . . . . . . . . 13
EXMID |
21 | | dmun 4827 |
. . . . . . . . . . . . . . 15
|
22 | 10 | uneq1i 3283 |
. . . . . . . . . . . . . . 15
|
23 | 14 | uneq2i 3284 |
. . . . . . . . . . . . . . 15
|
24 | 21, 22, 23 | 3eqtr2i 2202 |
. . . . . . . . . . . . . 14
|
25 | | f1rn 5414 |
. . . . . . . . . . . . . . . 16
|
26 | 25 | adantl 277 |
. . . . . . . . . . . . . . 15
EXMID
|
27 | | exmidexmid 4191 |
. . . . . . . . . . . . . . . . 17
EXMID
DECID
|
28 | 27 | ralrimivw 2549 |
. . . . . . . . . . . . . . . 16
EXMID
DECID
|
29 | 28 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
EXMID
DECID |
30 | | undifdcss 6912 |
. . . . . . . . . . . . . . 15
DECID
|
31 | 26, 29, 30 | sylanbrc 417 |
. . . . . . . . . . . . . 14
EXMID
|
32 | 24, 31 | eqtr4id 2227 |
. . . . . . . . . . . . 13
EXMID |
33 | | df-fn 5211 |
. . . . . . . . . . . . 13
|
34 | 20, 32, 33 | sylanbrc 417 |
. . . . . . . . . . . 12
EXMID |
35 | | rnun 5029 |
. . . . . . . . . . . . 13
|
36 | | dfdm4 4812 |
. . . . . . . . . . . . . . . 16
|
37 | | f1dm 5418 |
. . . . . . . . . . . . . . . 16
|
38 | 36, 37 | eqtr3id 2222 |
. . . . . . . . . . . . . . 15
|
39 | 38 | uneq1d 3286 |
. . . . . . . . . . . . . 14
|
40 | | exmidexmid 4191 |
. . . . . . . . . . . . . . . . . 18
EXMID
DECID |
41 | | exmiddc 836 |
. . . . . . . . . . . . . . . . . 18
DECID
|
42 | 40, 41 | syl 14 |
. . . . . . . . . . . . . . . . 17
EXMID
|
43 | | rnxpm 5050 |
. . . . . . . . . . . . . . . . . . . . 21
|
44 | 43 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | | snssi 3733 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | 45 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 44, 46 | eqsstrd 3189 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 47 | ex 115 |
. . . . . . . . . . . . . . . . . 18
|
49 | | notm0 3441 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | xpeq1 4634 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
51 | | 0xp 4700 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
52 | 50, 51 | eqtrdi 2224 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
53 | 52 | rneqd 4849 |
. . . . . . . . . . . . . . . . . . . . . 22
|
54 | | rn0 4876 |
. . . . . . . . . . . . . . . . . . . . . 22
|
55 | 53, 54 | eqtrdi 2224 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | | 0ss 3459 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | 55, 56 | eqsstrdi 3205 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 57 | a1d 22 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 49, 58 | sylbi 121 |
. . . . . . . . . . . . . . . . . 18
|
60 | 48, 59 | jaoi 716 |
. . . . . . . . . . . . . . . . 17
|
61 | 42, 60 | syl 14 |
. . . . . . . . . . . . . . . 16
EXMID |
62 | 61 | imp 124 |
. . . . . . . . . . . . . . 15
EXMID
|
63 | | ssequn2 3306 |
. . . . . . . . . . . . . . 15
|
64 | 62, 63 | sylib 122 |
. . . . . . . . . . . . . 14
EXMID
|
65 | 39, 64 | sylan9eqr 2230 |
. . . . . . . . . . . . 13
EXMID
|
66 | 35, 65 | eqtrid 2220 |
. . . . . . . . . . . 12
EXMID |
67 | | df-fo 5214 |
. . . . . . . . . . . 12
|
68 | 34, 66, 67 | sylanbrc 417 |
. . . . . . . . . . 11
EXMID |
69 | | vex 2738 |
. . . . . . . . . . . . . 14
|
70 | 69 | cnvex 5159 |
. . . . . . . . . . . . 13
|
71 | | vex 2738 |
. . . . . . . . . . . . . . 15
|
72 | | difexg 4139 |
. . . . . . . . . . . . . . 15
|
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
74 | 5 | snex 4180 |
. . . . . . . . . . . . . 14
|
75 | 73, 74 | xpex 4735 |
. . . . . . . . . . . . 13
|
76 | 70, 75 | unex 4435 |
. . . . . . . . . . . 12
|
77 | | foeq1 5426 |
. . . . . . . . . . . 12
|
78 | 76, 77 | spcev 2830 |
. . . . . . . . . . 11
|
79 | 68, 78 | syl 14 |
. . . . . . . . . 10
EXMID
|
80 | 79 | an32s 568 |
. . . . . . . . 9
EXMID |
81 | 80 | ex 115 |
. . . . . . . 8
EXMID
|
82 | 81 | exlimdv 1817 |
. . . . . . 7
EXMID
|
83 | 82 | imp 124 |
. . . . . 6
EXMID
|
84 | 83 | an32s 568 |
. . . . 5
EXMID |
85 | 84 | adantlrr 483 |
. . . 4
EXMID |
86 | 2, 85 | exlimddv 1896 |
. . 3
EXMID
|
87 | 86 | ex 115 |
. 2
EXMID |
88 | 87 | alrimivv 1873 |
1
EXMID |