Metamath Proof Explorer

Theorem nmulcom

Description: Natural multiplication commutes. (Contributed by Scott Fenton, 10-Jun-2026)

Ref Expression
Assertion nmulcom Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) = ( B .no A ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 oveq1 Could not format ( a = c -> ( a .no b ) = ( c .no b ) ) : No typesetting found for |- ( a = c -> ( a .no b ) = ( c .no b ) ) with typecode |-
2 oveq2 Could not format ( a = c -> ( b .no a ) = ( b .no c ) ) : No typesetting found for |- ( a = c -> ( b .no a ) = ( b .no c ) ) with typecode |-
3 1 2 eqeq12d Could not format ( a = c -> ( ( a .no b ) = ( b .no a ) <-> ( c .no b ) = ( b .no c ) ) ) : No typesetting found for |- ( a = c -> ( ( a .no b ) = ( b .no a ) <-> ( c .no b ) = ( b .no c ) ) ) with typecode |-
4 oveq2 Could not format ( b = d -> ( c .no b ) = ( c .no d ) ) : No typesetting found for |- ( b = d -> ( c .no b ) = ( c .no d ) ) with typecode |-
5 oveq1 Could not format ( b = d -> ( b .no c ) = ( d .no c ) ) : No typesetting found for |- ( b = d -> ( b .no c ) = ( d .no c ) ) with typecode |-
6 4 5 eqeq12d Could not format ( b = d -> ( ( c .no b ) = ( b .no c ) <-> ( c .no d ) = ( d .no c ) ) ) : No typesetting found for |- ( b = d -> ( ( c .no b ) = ( b .no c ) <-> ( c .no d ) = ( d .no c ) ) ) with typecode |-
7 oveq1 Could not format ( a = c -> ( a .no d ) = ( c .no d ) ) : No typesetting found for |- ( a = c -> ( a .no d ) = ( c .no d ) ) with typecode |-
8 oveq2 Could not format ( a = c -> ( d .no a ) = ( d .no c ) ) : No typesetting found for |- ( a = c -> ( d .no a ) = ( d .no c ) ) with typecode |-
9 7 8 eqeq12d Could not format ( a = c -> ( ( a .no d ) = ( d .no a ) <-> ( c .no d ) = ( d .no c ) ) ) : No typesetting found for |- ( a = c -> ( ( a .no d ) = ( d .no a ) <-> ( c .no d ) = ( d .no c ) ) ) with typecode |-
10 oveq1 Could not format ( a = A -> ( a .no b ) = ( A .no b ) ) : No typesetting found for |- ( a = A -> ( a .no b ) = ( A .no b ) ) with typecode |-
11 oveq2 Could not format ( a = A -> ( b .no a ) = ( b .no A ) ) : No typesetting found for |- ( a = A -> ( b .no a ) = ( b .no A ) ) with typecode |-
12 10 11 eqeq12d Could not format ( a = A -> ( ( a .no b ) = ( b .no a ) <-> ( A .no b ) = ( b .no A ) ) ) : No typesetting found for |- ( a = A -> ( ( a .no b ) = ( b .no a ) <-> ( A .no b ) = ( b .no A ) ) ) with typecode |-
13 oveq2 Could not format ( b = B -> ( A .no b ) = ( A .no B ) ) : No typesetting found for |- ( b = B -> ( A .no b ) = ( A .no B ) ) with typecode |-
14 oveq1 Could not format ( b = B -> ( b .no A ) = ( B .no A ) ) : No typesetting found for |- ( b = B -> ( b .no A ) = ( B .no A ) ) with typecode |-
15 13 14 eqeq12d Could not format ( b = B -> ( ( A .no b ) = ( b .no A ) <-> ( A .no B ) = ( B .no A ) ) ) : No typesetting found for |- ( b = B -> ( ( A .no b ) = ( b .no A ) <-> ( A .no B ) = ( B .no A ) ) ) with typecode |-
16 oveq1 Could not format ( c = z -> ( c .no b ) = ( z .no b ) ) : No typesetting found for |- ( c = z -> ( c .no b ) = ( z .no b ) ) with typecode |-
17 oveq2 Could not format ( c = z -> ( b .no c ) = ( b .no z ) ) : No typesetting found for |- ( c = z -> ( b .no c ) = ( b .no z ) ) with typecode |-
18 16 17 eqeq12d Could not format ( c = z -> ( ( c .no b ) = ( b .no c ) <-> ( z .no b ) = ( b .no z ) ) ) : No typesetting found for |- ( c = z -> ( ( c .no b ) = ( b .no c ) <-> ( z .no b ) = ( b .no z ) ) ) with typecode |-
19 simplr2 Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. c e. a ( c .no b ) = ( b .no c ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. c e. a ( c .no b ) = ( b .no c ) ) with typecode |-
20 simprl Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> z e. a ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> z e. a ) with typecode |-
21 18 19 20 rspcdva Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( z .no b ) = ( b .no z ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( z .no b ) = ( b .no z ) ) with typecode |-
22 oveq2 Could not format ( d = y -> ( a .no d ) = ( a .no y ) ) : No typesetting found for |- ( d = y -> ( a .no d ) = ( a .no y ) ) with typecode |-
23 oveq1 Could not format ( d = y -> ( d .no a ) = ( y .no a ) ) : No typesetting found for |- ( d = y -> ( d .no a ) = ( y .no a ) ) with typecode |-
24 22 23 eqeq12d Could not format ( d = y -> ( ( a .no d ) = ( d .no a ) <-> ( a .no y ) = ( y .no a ) ) ) : No typesetting found for |- ( d = y -> ( ( a .no d ) = ( d .no a ) <-> ( a .no y ) = ( y .no a ) ) ) with typecode |-
25 simplr3 Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. d e. b ( a .no d ) = ( d .no a ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. d e. b ( a .no d ) = ( d .no a ) ) with typecode |-
26 simprr Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> y e. b ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> y e. b ) with typecode |-
27 24 25 26 rspcdva Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( a .no y ) = ( y .no a ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( a .no y ) = ( y .no a ) ) with typecode |-
28 21 27 oveq12d Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( z .no b ) +no ( a .no y ) ) = ( ( b .no z ) +no ( y .no a ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( z .no b ) +no ( a .no y ) ) = ( ( b .no z ) +no ( y .no a ) ) ) with typecode |-
29 simpllr Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> b e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> b e. On ) with typecode |-
30 simplll Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> a e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> a e. On ) with typecode |-
31 onelon ⊢ a ∈ On ∧ z ∈ a → z ∈ On
32 30 20 31 syl2anc Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> z e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> z e. On ) with typecode |-
33 nmulcl Could not format ( ( b e. On /\ z e. On ) -> ( b .no z ) e. On ) : No typesetting found for |- ( ( b e. On /\ z e. On ) -> ( b .no z ) e. On ) with typecode |-
34 29 32 33 syl2anc Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( b .no z ) e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( b .no z ) e. On ) with typecode |-
35 onelon ⊢ b ∈ On ∧ y ∈ b → y ∈ On
36 29 26 35 syl2anc Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> y e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> y e. On ) with typecode |-
37 nmulcl Could not format ( ( y e. On /\ a e. On ) -> ( y .no a ) e. On ) : No typesetting found for |- ( ( y e. On /\ a e. On ) -> ( y .no a ) e. On ) with typecode |-
38 36 30 37 syl2anc Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( y .no a ) e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( y .no a ) e. On ) with typecode |-
39 naddcom Could not format ( ( ( b .no z ) e. On /\ ( y .no a ) e. On ) -> ( ( b .no z ) +no ( y .no a ) ) = ( ( y .no a ) +no ( b .no z ) ) ) : No typesetting found for |- ( ( ( b .no z ) e. On /\ ( y .no a ) e. On ) -> ( ( b .no z ) +no ( y .no a ) ) = ( ( y .no a ) +no ( b .no z ) ) ) with typecode |-
40 34 38 39 syl2anc Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( b .no z ) +no ( y .no a ) ) = ( ( y .no a ) +no ( b .no z ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( b .no z ) +no ( y .no a ) ) = ( ( y .no a ) +no ( b .no z ) ) ) with typecode |-
41 28 40 eqtrd Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( z .no b ) +no ( a .no y ) ) = ( ( y .no a ) +no ( b .no z ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( z .no b ) +no ( a .no y ) ) = ( ( y .no a ) +no ( b .no z ) ) ) with typecode |-
42 oveq1 Could not format ( c = z -> ( c .no d ) = ( z .no d ) ) : No typesetting found for |- ( c = z -> ( c .no d ) = ( z .no d ) ) with typecode |-
43 oveq2 Could not format ( c = z -> ( d .no c ) = ( d .no z ) ) : No typesetting found for |- ( c = z -> ( d .no c ) = ( d .no z ) ) with typecode |-
44 42 43 eqeq12d Could not format ( c = z -> ( ( c .no d ) = ( d .no c ) <-> ( z .no d ) = ( d .no z ) ) ) : No typesetting found for |- ( c = z -> ( ( c .no d ) = ( d .no c ) <-> ( z .no d ) = ( d .no z ) ) ) with typecode |-
45 oveq2 Could not format ( d = y -> ( z .no d ) = ( z .no y ) ) : No typesetting found for |- ( d = y -> ( z .no d ) = ( z .no y ) ) with typecode |-
46 oveq1 Could not format ( d = y -> ( d .no z ) = ( y .no z ) ) : No typesetting found for |- ( d = y -> ( d .no z ) = ( y .no z ) ) with typecode |-
47 45 46 eqeq12d Could not format ( d = y -> ( ( z .no d ) = ( d .no z ) <-> ( z .no y ) = ( y .no z ) ) ) : No typesetting found for |- ( d = y -> ( ( z .no d ) = ( d .no z ) <-> ( z .no y ) = ( y .no z ) ) ) with typecode |-
48 simplr1 Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. c e. a A. d e. b ( c .no d ) = ( d .no c ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> A. c e. a A. d e. b ( c .no d ) = ( d .no c ) ) with typecode |-
49 44 47 48 20 26 rspc2dv Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( z .no y ) = ( y .no z ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( z .no y ) = ( y .no z ) ) with typecode |-
50 49 oveq2d Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( x +no ( z .no y ) ) = ( x +no ( y .no z ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( x +no ( z .no y ) ) = ( x +no ( y .no z ) ) ) with typecode |-
51 41 50 eleq12d Could not format ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) /\ ( z e. a /\ y e. b ) ) -> ( ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) ) with typecode |-
52 51 2ralbidva Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> A. z e. a A. y e. b ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> A. z e. a A. y e. b ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) ) with typecode |-
53 ralcom Could not format ( A. z e. a A. y e. b ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) <-> A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) : No typesetting found for |- ( A. z e. a A. y e. b ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) <-> A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) with typecode |-
54 52 53 bitrdi Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) <-> A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) ) ) with typecode |-
55 54 rabbidv Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } = { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } = { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) with typecode |-
56 55 inteqd Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) with typecode |-
57 nmulval Could not format ( ( a e. On /\ b e. On ) -> ( a .no b ) = |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( a .no b ) = |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } ) with typecode |-
58 57 adantr Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( a .no b ) = |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( a .no b ) = |^| { x e. On | A. z e. a A. y e. b ( ( z .no b ) +no ( a .no y ) ) e. ( x +no ( z .no y ) ) } ) with typecode |-
59 nmulval Could not format ( ( b e. On /\ a e. On ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) : No typesetting found for |- ( ( b e. On /\ a e. On ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) with typecode |-
60 59 ancoms Could not format ( ( a e. On /\ b e. On ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) with typecode |-
61 60 adantr Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( b .no a ) = |^| { x e. On | A. y e. b A. z e. a ( ( y .no a ) +no ( b .no z ) ) e. ( x +no ( y .no z ) ) } ) with typecode |-
62 56 58 61 3eqtr4d Could not format ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( a .no b ) = ( b .no a ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) ) -> ( a .no b ) = ( b .no a ) ) with typecode |-
63 62 ex Could not format ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) -> ( a .no b ) = ( b .no a ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c .no d ) = ( d .no c ) /\ A. c e. a ( c .no b ) = ( b .no c ) /\ A. d e. b ( a .no d ) = ( d .no a ) ) -> ( a .no b ) = ( b .no a ) ) ) with typecode |-
64 3 6 9 12 15 63 on2ind Could not format ( ( A e. On /\ B e. On ) -> ( A .no B ) = ( B .no A ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A .no B ) = ( B .no A ) ) with typecode |-