Step | Hyp | Ref
| Expression |
1 | | brdomi 6611 |
. . . . 5
|
2 | 1 | ad2antll 482 |
. . . 4
EXMID
|
3 | | df-f1 5098 |
. . . . . . . . . . . . . . . . 17
|
4 | 3 | simprbi 273 |
. . . . . . . . . . . . . . . 16
|
5 | | vex 2663 |
. . . . . . . . . . . . . . . . . 18
|
6 | 5 | fconst 5288 |
. . . . . . . . . . . . . . . . 17
|
7 | | ffun 5245 |
. . . . . . . . . . . . . . . . 17
|
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
9 | 4, 8 | jctir 311 |
. . . . . . . . . . . . . . 15
|
10 | | df-rn 4520 |
. . . . . . . . . . . . . . . . . 18
|
11 | 10 | eqcomi 2121 |
. . . . . . . . . . . . . . . . 17
|
12 | 5 | snm 3613 |
. . . . . . . . . . . . . . . . . 18
|
13 | | dmxpm 4729 |
. . . . . . . . . . . . . . . . . 18
|
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
15 | 11, 14 | ineq12i 3245 |
. . . . . . . . . . . . . . . 16
|
16 | | disjdif 3405 |
. . . . . . . . . . . . . . . 16
|
17 | 15, 16 | eqtri 2138 |
. . . . . . . . . . . . . . 15
|
18 | | funun 5137 |
. . . . . . . . . . . . . . 15
|
19 | 9, 17, 18 | sylancl 409 |
. . . . . . . . . . . . . 14
|
20 | 19 | adantl 275 |
. . . . . . . . . . . . 13
EXMID |
21 | | f1rn 5299 |
. . . . . . . . . . . . . . . 16
|
22 | 21 | adantl 275 |
. . . . . . . . . . . . . . 15
EXMID
|
23 | | exmidexmid 4090 |
. . . . . . . . . . . . . . . . 17
EXMID
DECID
|
24 | 23 | ralrimivw 2483 |
. . . . . . . . . . . . . . . 16
EXMID
DECID
|
25 | 24 | ad2antrr 479 |
. . . . . . . . . . . . . . 15
EXMID
DECID |
26 | | undifdcss 6779 |
. . . . . . . . . . . . . . 15
DECID
|
27 | 22, 25, 26 | sylanbrc 413 |
. . . . . . . . . . . . . 14
EXMID
|
28 | | dmun 4716 |
. . . . . . . . . . . . . . 15
|
29 | 10 | uneq1i 3196 |
. . . . . . . . . . . . . . 15
|
30 | 14 | uneq2i 3197 |
. . . . . . . . . . . . . . 15
|
31 | 28, 29, 30 | 3eqtr2i 2144 |
. . . . . . . . . . . . . 14
|
32 | 27, 31 | syl6reqr 2169 |
. . . . . . . . . . . . 13
EXMID |
33 | | df-fn 5096 |
. . . . . . . . . . . . 13
|
34 | 20, 32, 33 | sylanbrc 413 |
. . . . . . . . . . . 12
EXMID |
35 | | rnun 4917 |
. . . . . . . . . . . . 13
|
36 | | dfdm4 4701 |
. . . . . . . . . . . . . . . 16
|
37 | | f1dm 5303 |
. . . . . . . . . . . . . . . 16
|
38 | 36, 37 | syl5eqr 2164 |
. . . . . . . . . . . . . . 15
|
39 | 38 | uneq1d 3199 |
. . . . . . . . . . . . . 14
|
40 | | exmidexmid 4090 |
. . . . . . . . . . . . . . . . . 18
EXMID
DECID |
41 | | exmiddc 806 |
. . . . . . . . . . . . . . . . . 18
DECID
|
42 | 40, 41 | syl 14 |
. . . . . . . . . . . . . . . . 17
EXMID
|
43 | | rnxpm 4938 |
. . . . . . . . . . . . . . . . . . . . 21
|
44 | 43 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
|
45 | | snssi 3634 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | 45 | adantl 275 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 44, 46 | eqsstrd 3103 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 47 | ex 114 |
. . . . . . . . . . . . . . . . . 18
|
49 | | notm0 3353 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | xpeq1 4523 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
51 | | 0xp 4589 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
52 | 50, 51 | syl6eq 2166 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
53 | 52 | rneqd 4738 |
. . . . . . . . . . . . . . . . . . . . . 22
|
54 | | rn0 4765 |
. . . . . . . . . . . . . . . . . . . . . 22
|
55 | 53, 54 | syl6eq 2166 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | | 0ss 3371 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | 55, 56 | eqsstrdi 3119 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 57 | a1d 22 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 49, 58 | sylbi 120 |
. . . . . . . . . . . . . . . . . 18
|
60 | 48, 59 | jaoi 690 |
. . . . . . . . . . . . . . . . 17
|
61 | 42, 60 | syl 14 |
. . . . . . . . . . . . . . . 16
EXMID |
62 | 61 | imp 123 |
. . . . . . . . . . . . . . 15
EXMID
|
63 | | ssequn2 3219 |
. . . . . . . . . . . . . . 15
|
64 | 62, 63 | sylib 121 |
. . . . . . . . . . . . . 14
EXMID
|
65 | 39, 64 | sylan9eqr 2172 |
. . . . . . . . . . . . 13
EXMID
|
66 | 35, 65 | syl5eq 2162 |
. . . . . . . . . . . 12
EXMID |
67 | | df-fo 5099 |
. . . . . . . . . . . 12
|
68 | 34, 66, 67 | sylanbrc 413 |
. . . . . . . . . . 11
EXMID |
69 | | vex 2663 |
. . . . . . . . . . . . . 14
|
70 | 69 | cnvex 5047 |
. . . . . . . . . . . . 13
|
71 | | vex 2663 |
. . . . . . . . . . . . . . 15
|
72 | | difexg 4039 |
. . . . . . . . . . . . . . 15
|
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
74 | 5 | snex 4079 |
. . . . . . . . . . . . . 14
|
75 | 73, 74 | xpex 4624 |
. . . . . . . . . . . . 13
|
76 | 70, 75 | unex 4332 |
. . . . . . . . . . . 12
|
77 | | foeq1 5311 |
. . . . . . . . . . . 12
|
78 | 76, 77 | spcev 2754 |
. . . . . . . . . . 11
|
79 | 68, 78 | syl 14 |
. . . . . . . . . 10
EXMID
|
80 | 79 | an32s 542 |
. . . . . . . . 9
EXMID |
81 | 80 | ex 114 |
. . . . . . . 8
EXMID
|
82 | 81 | exlimdv 1775 |
. . . . . . 7
EXMID
|
83 | 82 | imp 123 |
. . . . . 6
EXMID
|
84 | 83 | an32s 542 |
. . . . 5
EXMID |
85 | 84 | adantlrr 474 |
. . . 4
EXMID |
86 | 2, 85 | exlimddv 1854 |
. . 3
EXMID
|
87 | 86 | ex 114 |
. 2
EXMID |
88 | 87 | alrimivv 1831 |
1
EXMID |