Step |
Hyp |
Ref |
Expression |
1 |
|
issgrpn0.b |
|
2 |
|
issgrpn0.o |
Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |- |
3 |
|
simpl1 |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> X e. B ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> X e. B ) with typecode |- |
4 |
|
oveq1 |
Could not format ( x = X -> ( x .o. y ) = ( X .o. y ) ) : No typesetting found for |- ( x = X -> ( x .o. y ) = ( X .o. y ) ) with typecode |- |
5 |
4
|
oveq1d |
Could not format ( x = X -> ( ( x .o. y ) .o. z ) = ( ( X .o. y ) .o. z ) ) : No typesetting found for |- ( x = X -> ( ( x .o. y ) .o. z ) = ( ( X .o. y ) .o. z ) ) with typecode |- |
6 |
|
oveq1 |
Could not format ( x = X -> ( x .o. ( y .o. z ) ) = ( X .o. ( y .o. z ) ) ) : No typesetting found for |- ( x = X -> ( x .o. ( y .o. z ) ) = ( X .o. ( y .o. z ) ) ) with typecode |- |
7 |
5 6
|
eqeq12d |
Could not format ( x = X -> ( ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( x = X -> ( ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |- |
8 |
7
|
notbid |
Could not format ( x = X -> ( -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( x = X -> ( -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |- |
9 |
8
|
rexbidv |
Could not format ( x = X -> ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( x = X -> ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |- |
10 |
9
|
rexbidv |
Could not format ( x = X -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( x = X -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |- |
11 |
10
|
adantl |
Could not format ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ x = X ) -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ x = X ) -> ( E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) ) with typecode |- |
12 |
|
simpl2 |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Y e. B ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Y e. B ) with typecode |- |
13 |
|
oveq2 |
Could not format ( y = Y -> ( X .o. y ) = ( X .o. Y ) ) : No typesetting found for |- ( y = Y -> ( X .o. y ) = ( X .o. Y ) ) with typecode |- |
14 |
13
|
oveq1d |
Could not format ( y = Y -> ( ( X .o. y ) .o. z ) = ( ( X .o. Y ) .o. z ) ) : No typesetting found for |- ( y = Y -> ( ( X .o. y ) .o. z ) = ( ( X .o. Y ) .o. z ) ) with typecode |- |
15 |
|
oveq1 |
Could not format ( y = Y -> ( y .o. z ) = ( Y .o. z ) ) : No typesetting found for |- ( y = Y -> ( y .o. z ) = ( Y .o. z ) ) with typecode |- |
16 |
15
|
oveq2d |
Could not format ( y = Y -> ( X .o. ( y .o. z ) ) = ( X .o. ( Y .o. z ) ) ) : No typesetting found for |- ( y = Y -> ( X .o. ( y .o. z ) ) = ( X .o. ( Y .o. z ) ) ) with typecode |- |
17 |
14 16
|
eqeq12d |
Could not format ( y = Y -> ( ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) : No typesetting found for |- ( y = Y -> ( ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) with typecode |- |
18 |
17
|
notbid |
Could not format ( y = Y -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) : No typesetting found for |- ( y = Y -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) with typecode |- |
19 |
18
|
adantl |
Could not format ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) : No typesetting found for |- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) with typecode |- |
20 |
19
|
rexbidv |
Could not format ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) : No typesetting found for |- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ y = Y ) -> ( E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) <-> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) ) with typecode |- |
21 |
|
simpl3 |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Z e. B ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> Z e. B ) with typecode |- |
22 |
|
oveq2 |
Could not format ( z = Z -> ( ( X .o. Y ) .o. z ) = ( ( X .o. Y ) .o. Z ) ) : No typesetting found for |- ( z = Z -> ( ( X .o. Y ) .o. z ) = ( ( X .o. Y ) .o. Z ) ) with typecode |- |
23 |
|
oveq2 |
Could not format ( z = Z -> ( Y .o. z ) = ( Y .o. Z ) ) : No typesetting found for |- ( z = Z -> ( Y .o. z ) = ( Y .o. Z ) ) with typecode |- |
24 |
23
|
oveq2d |
Could not format ( z = Z -> ( X .o. ( Y .o. z ) ) = ( X .o. ( Y .o. Z ) ) ) : No typesetting found for |- ( z = Z -> ( X .o. ( Y .o. z ) ) = ( X .o. ( Y .o. Z ) ) ) with typecode |- |
25 |
22 24
|
eqeq12d |
Could not format ( z = Z -> ( ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) : No typesetting found for |- ( z = Z -> ( ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) with typecode |- |
26 |
25
|
notbid |
Could not format ( z = Z -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) : No typesetting found for |- ( z = Z -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) with typecode |- |
27 |
26
|
adantl |
Could not format ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ z = Z ) -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) : No typesetting found for |- ( ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) /\ z = Z ) -> ( -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) <-> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) ) with typecode |- |
28 |
|
neneq |
Could not format ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) : No typesetting found for |- ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) with typecode |- |
29 |
28
|
adantl |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( ( X .o. Y ) .o. Z ) = ( X .o. ( Y .o. Z ) ) ) with typecode |- |
30 |
21 27 29
|
rspcedvd |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. z e. B -. ( ( X .o. Y ) .o. z ) = ( X .o. ( Y .o. z ) ) ) with typecode |- |
31 |
12 20 30
|
rspcedvd |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. y e. B E. z e. B -. ( ( X .o. y ) .o. z ) = ( X .o. ( y .o. z ) ) ) with typecode |- |
32 |
3 11 31
|
rspcedvd |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |- |
33 |
|
rexnal |
Could not format ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |- |
34 |
33
|
2rexbii |
Could not format ( E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |- |
35 |
|
rexnal2 |
Could not format ( E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( E. x e. B E. y e. B -. A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |- |
36 |
34 35
|
bitr2i |
Could not format ( -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) <-> E. x e. B E. y e. B E. z e. B -. ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |- |
37 |
32 36
|
sylibr |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |- |
38 |
37
|
intnand |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |- |
39 |
1 2
|
issgrp |
Could not format ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M e. Mgm /\ A. x e. B A. y e. B A. z e. B ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |- |
40 |
38 39
|
sylnibr |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. M e. Smgrp ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> -. M e. Smgrp ) with typecode |- |
41 |
|
df-nel |
Could not format ( M e/ Smgrp <-> -. M e. Smgrp ) : No typesetting found for |- ( M e/ Smgrp <-> -. M e. Smgrp ) with typecode |- |
42 |
40 41
|
sylibr |
Could not format ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> M e/ Smgrp ) : No typesetting found for |- ( ( ( X e. B /\ Y e. B /\ Z e. B ) /\ ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) ) -> M e/ Smgrp ) with typecode |- |
43 |
42
|
ex |
Could not format ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) ) : No typesetting found for |- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( ( X .o. Y ) .o. Z ) =/= ( X .o. ( Y .o. Z ) ) -> M e/ Smgrp ) ) with typecode |- |