Proof of Theorem ntrneix13
Step | Hyp | Ref
| Expression |
1 | | dfss3 3592 |
. . . . . . . . 9
|
2 | | ntrnei.o |
. . . . . . . . . . . . . . 15
|
3 | | ntrnei.f |
. . . . . . . . . . . . . . 15
|
4 | | ntrnei.r |
. . . . . . . . . . . . . . 15
|
5 | 2, 3, 4 | ntrneiiex 38374 |
. . . . . . . . . . . . . 14
|
6 | 5 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
7 | | elmapi 7879 |
. . . . . . . . . . . . 13
|
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
|
9 | 2, 3, 4 | ntrneibex 38371 |
. . . . . . . . . . . . . 14
|
10 | 9 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
11 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
12 | 11 | elpwid 4170 |
. . . . . . . . . . . . . 14
|
13 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
14 | 13 | elpwid 4170 |
. . . . . . . . . . . . . 14
|
15 | 12, 14 | unssd 3789 |
. . . . . . . . . . . . 13
|
16 | 10, 15 | sselpwd 4807 |
. . . . . . . . . . . 12
|
17 | 8, 16 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
18 | 17 | elpwid 4170 |
. . . . . . . . . 10
|
19 | | ralss 3668 |
. . . . . . . . . 10
|
20 | 18, 19 | syl 17 |
. . . . . . . . 9
|
21 | 1, 20 | syl5bb 272 |
. . . . . . . 8
|
22 | | dfss3 3592 |
. . . . . . . . 9
|
23 | 8, 11 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
24 | 23 | elpwid 4170 |
. . . . . . . . . . 11
|
25 | 8, 13 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
26 | 25 | elpwid 4170 |
. . . . . . . . . . 11
|
27 | 24, 26 | unssd 3789 |
. . . . . . . . . 10
|
28 | | ralss 3668 |
. . . . . . . . . 10
|
29 | 27, 28 | syl 17 |
. . . . . . . . 9
|
30 | 22, 29 | syl5bb 272 |
. . . . . . . 8
|
31 | 21, 30 | anbi12d 747 |
. . . . . . 7
|
32 | | eqss 3618 |
. . . . . . 7
|
33 | | ralbiim 3069 |
. . . . . . 7
|
34 | 31, 32, 33 | 3bitr4g 303 |
. . . . . 6
|
35 | 4 | ad3antrrr 766 |
. . . . . . . . 9
|
36 | | simpr 477 |
. . . . . . . . 9
|
37 | 9 | ad3antrrr 766 |
. . . . . . . . . 10
|
38 | | simpllr 799 |
. . . . . . . . . . . 12
|
39 | 38 | elpwid 4170 |
. . . . . . . . . . 11
|
40 | | simplr 792 |
. . . . . . . . . . . 12
|
41 | 40 | elpwid 4170 |
. . . . . . . . . . 11
|
42 | 39, 41 | unssd 3789 |
. . . . . . . . . 10
|
43 | 37, 42 | sselpwd 4807 |
. . . . . . . . 9
|
44 | 2, 3, 35, 36, 43 | ntrneiel 38379 |
. . . . . . . 8
|
45 | | elun 3753 |
. . . . . . . . 9
|
46 | 2, 3, 35, 36, 38 | ntrneiel 38379 |
. . . . . . . . . 10
|
47 | 2, 3, 35, 36, 40 | ntrneiel 38379 |
. . . . . . . . . 10
|
48 | 46, 47 | orbi12d 746 |
. . . . . . . . 9
|
49 | 45, 48 | syl5bb 272 |
. . . . . . . 8
|
50 | 44, 49 | bibi12d 335 |
. . . . . . 7
|
51 | 50 | ralbidva 2985 |
. . . . . 6
|
52 | 34, 51 | bitrd 268 |
. . . . 5
|
53 | 52 | ralbidva 2985 |
. . . 4
|
54 | | ralcom 3098 |
. . . 4
|
55 | 53, 54 | syl6bb 276 |
. . 3
|
56 | 55 | ralbidva 2985 |
. 2
|
57 | | ralcom 3098 |
. 2
|
58 | 56, 57 | syl6bb 276 |
1
|