Step |
Hyp |
Ref |
Expression |
1 |
|
isirred2.1 |
|- B = ( Base ` R ) |
2 |
|
isirred2.2 |
|- U = ( Unit ` R ) |
3 |
|
isirred2.3 |
|- I = ( Irred ` R ) |
4 |
|
isirred2.4 |
|- .x. = ( .r ` R ) |
5 |
|
eldif |
|- ( X e. ( B \ U ) <-> ( X e. B /\ -. X e. U ) ) |
6 |
|
eldif |
|- ( x e. ( B \ U ) <-> ( x e. B /\ -. x e. U ) ) |
7 |
|
eldif |
|- ( y e. ( B \ U ) <-> ( y e. B /\ -. y e. U ) ) |
8 |
6 7
|
anbi12i |
|- ( ( x e. ( B \ U ) /\ y e. ( B \ U ) ) <-> ( ( x e. B /\ -. x e. U ) /\ ( y e. B /\ -. y e. U ) ) ) |
9 |
|
an4 |
|- ( ( ( x e. B /\ -. x e. U ) /\ ( y e. B /\ -. y e. U ) ) <-> ( ( x e. B /\ y e. B ) /\ ( -. x e. U /\ -. y e. U ) ) ) |
10 |
8 9
|
bitri |
|- ( ( x e. ( B \ U ) /\ y e. ( B \ U ) ) <-> ( ( x e. B /\ y e. B ) /\ ( -. x e. U /\ -. y e. U ) ) ) |
11 |
10
|
imbi1i |
|- ( ( ( x e. ( B \ U ) /\ y e. ( B \ U ) ) -> ( x .x. y ) =/= X ) <-> ( ( ( x e. B /\ y e. B ) /\ ( -. x e. U /\ -. y e. U ) ) -> ( x .x. y ) =/= X ) ) |
12 |
|
impexp |
|- ( ( ( ( x e. B /\ y e. B ) /\ ( -. x e. U /\ -. y e. U ) ) -> ( x .x. y ) =/= X ) <-> ( ( x e. B /\ y e. B ) -> ( ( -. x e. U /\ -. y e. U ) -> ( x .x. y ) =/= X ) ) ) |
13 |
|
pm4.56 |
|- ( ( -. x e. U /\ -. y e. U ) <-> -. ( x e. U \/ y e. U ) ) |
14 |
|
df-ne |
|- ( ( x .x. y ) =/= X <-> -. ( x .x. y ) = X ) |
15 |
13 14
|
imbi12i |
|- ( ( ( -. x e. U /\ -. y e. U ) -> ( x .x. y ) =/= X ) <-> ( -. ( x e. U \/ y e. U ) -> -. ( x .x. y ) = X ) ) |
16 |
|
con34b |
|- ( ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) <-> ( -. ( x e. U \/ y e. U ) -> -. ( x .x. y ) = X ) ) |
17 |
15 16
|
bitr4i |
|- ( ( ( -. x e. U /\ -. y e. U ) -> ( x .x. y ) =/= X ) <-> ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) |
18 |
17
|
imbi2i |
|- ( ( ( x e. B /\ y e. B ) -> ( ( -. x e. U /\ -. y e. U ) -> ( x .x. y ) =/= X ) ) <-> ( ( x e. B /\ y e. B ) -> ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) ) |
19 |
12 18
|
bitri |
|- ( ( ( ( x e. B /\ y e. B ) /\ ( -. x e. U /\ -. y e. U ) ) -> ( x .x. y ) =/= X ) <-> ( ( x e. B /\ y e. B ) -> ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) ) |
20 |
11 19
|
bitri |
|- ( ( ( x e. ( B \ U ) /\ y e. ( B \ U ) ) -> ( x .x. y ) =/= X ) <-> ( ( x e. B /\ y e. B ) -> ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) ) |
21 |
20
|
2albii |
|- ( A. x A. y ( ( x e. ( B \ U ) /\ y e. ( B \ U ) ) -> ( x .x. y ) =/= X ) <-> A. x A. y ( ( x e. B /\ y e. B ) -> ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) ) |
22 |
|
r2al |
|- ( A. x e. ( B \ U ) A. y e. ( B \ U ) ( x .x. y ) =/= X <-> A. x A. y ( ( x e. ( B \ U ) /\ y e. ( B \ U ) ) -> ( x .x. y ) =/= X ) ) |
23 |
|
r2al |
|- ( A. x e. B A. y e. B ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) <-> A. x A. y ( ( x e. B /\ y e. B ) -> ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) ) |
24 |
21 22 23
|
3bitr4i |
|- ( A. x e. ( B \ U ) A. y e. ( B \ U ) ( x .x. y ) =/= X <-> A. x e. B A. y e. B ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) |
25 |
5 24
|
anbi12i |
|- ( ( X e. ( B \ U ) /\ A. x e. ( B \ U ) A. y e. ( B \ U ) ( x .x. y ) =/= X ) <-> ( ( X e. B /\ -. X e. U ) /\ A. x e. B A. y e. B ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) ) |
26 |
|
eqid |
|- ( B \ U ) = ( B \ U ) |
27 |
1 2 3 26 4
|
isirred |
|- ( X e. I <-> ( X e. ( B \ U ) /\ A. x e. ( B \ U ) A. y e. ( B \ U ) ( x .x. y ) =/= X ) ) |
28 |
|
df-3an |
|- ( ( X e. B /\ -. X e. U /\ A. x e. B A. y e. B ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) <-> ( ( X e. B /\ -. X e. U ) /\ A. x e. B A. y e. B ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) ) |
29 |
25 27 28
|
3bitr4i |
|- ( X e. I <-> ( X e. B /\ -. X e. U /\ A. x e. B A. y e. B ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) ) |