Step | Hyp | Ref
| Expression |
1 | | orc 400 |
. . . . 5
|
2 | 1 | a1d 25 |
. . . 4
|
3 | | eliun 4524 |
. . . . . . . . . 10
|
4 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
5 | 4 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
6 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
7 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
8 | | otthg 4954 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
9 | 5, 6, 7, 8 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
10 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
11 | 9, 10 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . 22
|
12 | 11 | con3d 148 |
. . . . . . . . . . . . . . . . . . . . 21
|
13 | 12 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
|
14 | 13 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
|
15 | 14 | imp31 448 |
. . . . . . . . . . . . . . . . . 18
|
16 | 15 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
18 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . 19
|
19 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . 20
|
20 | 19 | notbid 308 |
. . . . . . . . . . . . . . . . . . 19
|
21 | 18, 20 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
|
22 | 21 | adantl 482 |
. . . . . . . . . . . . . . . . 17
|
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
24 | 17, 23 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
25 | | velsn 4193 |
. . . . . . . . . . . . . . 15
|
26 | 24, 25 | sylnibr 319 |
. . . . . . . . . . . . . 14
|
27 | 26 | nrexdv 3001 |
. . . . . . . . . . . . 13
|
28 | | eliun 4524 |
. . . . . . . . . . . . 13
|
29 | 27, 28 | sylnibr 319 |
. . . . . . . . . . . 12
|
30 | 29 | ex 450 |
. . . . . . . . . . 11
|
31 | 30 | rexlimdva 3031 |
. . . . . . . . . 10
|
32 | 3, 31 | syl5bi 232 |
. . . . . . . . 9
|
33 | 32 | ralrimiv 2965 |
. . . . . . . 8
|
34 | | oteq3 4413 |
. . . . . . . . . . . . 13
|
35 | 34 | sneqd 4189 |
. . . . . . . . . . . 12
|
36 | 35 | cbviunv 4559 |
. . . . . . . . . . 11
|
37 | 36 | eleq2i 2693 |
. . . . . . . . . 10
|
38 | 37 | notbii 310 |
. . . . . . . . 9
|
39 | 38 | ralbii 2980 |
. . . . . . . 8
|
40 | 33, 39 | sylibr 224 |
. . . . . . 7
|
41 | | disj 4017 |
. . . . . . 7
|
42 | 40, 41 | sylibr 224 |
. . . . . 6
|
43 | 42 | olcd 408 |
. . . . 5
|
44 | 43 | ex 450 |
. . . 4
|
45 | 2, 44 | pm2.61i 176 |
. . 3
|
46 | 45 | ralrimivva 2971 |
. 2
|
47 | | oteq1 4411 |
. . . . 5
|
48 | 47 | sneqd 4189 |
. . . 4
|
49 | 48 | iuneq2d 4547 |
. . 3
|
50 | 49 | disjor 4634 |
. 2
Disj
|
51 | 46, 50 | sylibr 224 |
1
Disj |