Step | Hyp | Ref
| Expression |
1 | | elfvdm 6220 |
. . . 4
Irred
Irred |
2 | | irred.3 |
. . . 4
Irred |
3 | 1, 2 | eleq2s 2719 |
. . 3
Irred |
4 | | elex 3212 |
. . 3
Irred |
5 | 3, 4 | syl 17 |
. 2
|
6 | | eldifi 3732 |
. . . . . 6
|
7 | | irred.4 |
. . . . . 6
|
8 | 6, 7 | eleq2s 2719 |
. . . . 5
|
9 | | irred.1 |
. . . . 5
|
10 | 8, 9 | syl6eleq 2711 |
. . . 4
|
11 | 10 | elfvexd 6222 |
. . 3
|
12 | 11 | adantr 481 |
. 2
|
13 | | fvex 6201 |
. . . . . . . 8
|
14 | | difexg 4808 |
. . . . . . . 8
Unit |
15 | 13, 14 | mp1i 13 |
. . . . . . 7
Unit |
16 | | simpr 477 |
. . . . . . . . 9
Unit Unit |
17 | | simpl 473 |
. . . . . . . . . . . . 13
Unit |
18 | 17 | fveq2d 6195 |
. . . . . . . . . . . 12
Unit |
19 | 18, 9 | syl6eqr 2674 |
. . . . . . . . . . 11
Unit |
20 | 17 | fveq2d 6195 |
. . . . . . . . . . . 12
Unit Unit Unit |
21 | | irred.2 |
. . . . . . . . . . . 12
Unit |
22 | 20, 21 | syl6eqr 2674 |
. . . . . . . . . . 11
Unit Unit |
23 | 19, 22 | difeq12d 3729 |
. . . . . . . . . 10
Unit Unit |
24 | 23, 7 | syl6eqr 2674 |
. . . . . . . . 9
Unit Unit |
25 | 16, 24 | eqtrd 2656 |
. . . . . . . 8
Unit |
26 | 17 | fveq2d 6195 |
. . . . . . . . . . . . 13
Unit |
27 | | irred.5 |
. . . . . . . . . . . . 13
|
28 | 26, 27 | syl6eqr 2674 |
. . . . . . . . . . . 12
Unit |
29 | 28 | oveqd 6667 |
. . . . . . . . . . 11
Unit |
30 | 29 | neeq1d 2853 |
. . . . . . . . . 10
Unit
|
31 | 25, 30 | raleqbidv 3152 |
. . . . . . . . 9
Unit
|
32 | 25, 31 | raleqbidv 3152 |
. . . . . . . 8
Unit
|
33 | 25, 32 | rabeqbidv 3195 |
. . . . . . 7
Unit
|
34 | 15, 33 | csbied 3560 |
. . . . . 6
Unit
|
35 | | df-irred 18643 |
. . . . . 6
Irred
Unit |
36 | | fvex 6201 |
. . . . . . . . . 10
|
37 | 9, 36 | eqeltri 2697 |
. . . . . . . . 9
|
38 | | difexg 4808 |
. . . . . . . . 9
|
39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
|
40 | 7, 39 | eqeltri 2697 |
. . . . . . 7
|
41 | 40 | rabex 4813 |
. . . . . 6
|
42 | 34, 35, 41 | fvmpt 6282 |
. . . . 5
Irred
|
43 | 2, 42 | syl5eq 2668 |
. . . 4
|
44 | 43 | eleq2d 2687 |
. . 3
|
45 | | neeq2 2857 |
. . . . 5
|
46 | 45 | 2ralbidv 2989 |
. . . 4
|
47 | 46 | elrab 3363 |
. . 3
|
48 | 44, 47 | syl6bb 276 |
. 2
|
49 | 5, 12, 48 | pm5.21nii 368 |
1
|