Step |
Hyp |
Ref |
Expression |
1 |
|
prmidlval.1 |
|
2 |
|
prmidlval.2 |
|
3 |
|
simpr |
|
4 |
|
simplrr |
|
5 |
|
eqid |
|
6 |
1 5
|
lidlss |
|
7 |
4 6
|
syl |
|
8 |
|
simplrl |
|
9 |
1 5
|
lidlss |
|
10 |
8 9
|
syl |
|
11 |
|
simpllr |
|
12 |
|
ssralv |
|
13 |
10 11 12
|
sylc |
|
14 |
|
ssralv |
|
15 |
14
|
ralimdv |
|
16 |
7 13 15
|
sylc |
|
17 |
|
r19.26-2 |
|
18 |
|
pm3.35 |
|
19 |
18
|
2ralimi |
|
20 |
17 19
|
sylbir |
|
21 |
3 16 20
|
syl2anc |
|
22 |
|
2ralor |
|
23 |
|
dfss3 |
|
24 |
|
dfss3 |
|
25 |
23 24
|
orbi12i |
|
26 |
22 25
|
sylbb2 |
|
27 |
21 26
|
syl |
|
28 |
27
|
ex |
|
29 |
28
|
ralrimivva |
|
30 |
1 2
|
isprmidl |
Could not format ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) : No typesetting found for |- ( R e. Ring -> ( P e. ( PrmIdeal ` R ) <-> ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) ) with typecode |- |
31 |
30
|
biimpar |
Could not format ( ( R e. Ring /\ ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ ( P e. ( LIdeal ` R ) /\ P =/= B /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode |- |
32 |
31
|
3anassrs |
Could not format ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. a e. ( LIdeal ` R ) A. b e. ( LIdeal ` R ) ( A. x e. a A. y e. b ( x .x. y ) e. P -> ( a C_ P \/ b C_ P ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode |- |
33 |
29 32
|
syldan |
Could not format ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ P =/= B ) /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode |- |
34 |
33
|
anasss |
Could not format ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. Ring /\ P e. ( LIdeal ` R ) ) /\ ( P =/= B /\ A. x e. B A. y e. B ( ( x .x. y ) e. P -> ( x e. P \/ y e. P ) ) ) ) -> P e. ( PrmIdeal ` R ) ) with typecode |- |