Step | Hyp | Ref
| Expression |
1 | | porpss 6941 |
. . . 4
[] |
2 | | cnvpo 5673 |
. . . 4
[]
[] |
3 | 1, 2 | mpbi 220 |
. . 3
[] |
4 | | pwfi 8261 |
. . . 4
|
5 | 4 | biimpi 206 |
. . 3
|
6 | | frfi 8205 |
. . 3
[]
[] |
7 | 3, 5, 6 | sylancr 695 |
. 2
[] |
8 | | inss2 3834 |
. . . . . 6
|
9 | | pwexg 4850 |
. . . . . 6
|
10 | | ssexg 4804 |
. . . . . 6
|
11 | 8, 9, 10 | sylancr 695 |
. . . . 5
|
12 | | 0fin 8188 |
. . . . . . . 8
|
13 | | 0elpw 4834 |
. . . . . . . 8
|
14 | | elin 3796 |
. . . . . . . 8
|
15 | 12, 13, 14 | mpbir2an 955 |
. . . . . . 7
|
16 | 15 | ne0ii 3923 |
. . . . . 6
|
17 | | fri 5076 |
. . . . . 6
[]
[] |
18 | 8, 16, 17 | mpanr12 721 |
. . . . 5
[]
[] |
19 | 11, 18 | sylan 488 |
. . . 4
[]
[] |
20 | 19 | ex 450 |
. . 3
[] [] |
21 | | inss1 3833 |
. . . . . 6
|
22 | | simpl 473 |
. . . . . 6
[]
|
23 | 21, 22 | sseldi 3601 |
. . . . 5
[]
|
24 | | ralnex 2992 |
. . . . . . . 8
[] [] |
25 | 21 | sseli 3599 |
. . . . . . . . . . . . . 14
|
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
|
27 | | snfi 8038 |
. . . . . . . . . . . . 13
|
28 | | unfi 8227 |
. . . . . . . . . . . . 13
|
29 | 26, 27, 28 | sylancl 694 |
. . . . . . . . . . . 12
|
30 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
|
31 | 30 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | elpwid 4170 |
. . . . . . . . . . . . . . 15
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . . 14
|
34 | | snssi 4339 |
. . . . . . . . . . . . . . 15
|
35 | 34 | ad2antrl 764 |
. . . . . . . . . . . . . 14
|
36 | 33, 35 | unssd 3789 |
. . . . . . . . . . . . 13
|
37 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
38 | | snex 4908 |
. . . . . . . . . . . . . . 15
|
39 | 37, 38 | unex 6956 |
. . . . . . . . . . . . . 14
|
40 | 39 | elpw 4164 |
. . . . . . . . . . . . 13
|
41 | 36, 40 | sylibr 224 |
. . . . . . . . . . . 12
|
42 | 29, 41 | elind 3798 |
. . . . . . . . . . 11
|
43 | | disjsn 4246 |
. . . . . . . . . . . . . . 15
|
44 | 43 | biimpri 218 |
. . . . . . . . . . . . . 14
|
45 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
46 | 45 | snnz 4309 |
. . . . . . . . . . . . . 14
|
47 | | disjpss 4028 |
. . . . . . . . . . . . . 14
|
48 | 44, 46, 47 | sylancl 694 |
. . . . . . . . . . . . 13
|
49 | 48 | ad2antll 765 |
. . . . . . . . . . . 12
|
50 | 39, 37 | brcnv 5305 |
. . . . . . . . . . . . 13
[] [] |
51 | 39 | brrpss 6940 |
. . . . . . . . . . . . 13
[]
|
52 | 50, 51 | bitri 264 |
. . . . . . . . . . . 12
[] |
53 | 49, 52 | sylibr 224 |
. . . . . . . . . . 11
[] |
54 | | breq1 4656 |
. . . . . . . . . . . 12
[]
[] |
55 | 54 | rspcev 3309 |
. . . . . . . . . . 11
[]
[] |
56 | 42, 53, 55 | syl2anc 693 |
. . . . . . . . . 10
[] |
57 | 56 | expr 643 |
. . . . . . . . 9
[] |
58 | 57 | con1d 139 |
. . . . . . . 8
[]
|
59 | 24, 58 | syl5bi 232 |
. . . . . . 7
[] |
60 | 59 | impancom 456 |
. . . . . 6
[]
|
61 | 60 | ssrdv 3609 |
. . . . 5
[]
|
62 | | ssfi 8180 |
. . . . 5
|
63 | 23, 61, 62 | syl2anc 693 |
. . . 4
[]
|
64 | 63 | rexlimiva 3028 |
. . 3
[] |
65 | 20, 64 | syl6 35 |
. 2
[] |
66 | 7, 65 | impbid2 216 |
1
[] |