Theorem nmulprop

Description: Show closure and value of natural multiplication. (Contributed by Scott Fenton, 2-Jun-2026)

	Ref	Expression
Assertion	nmulprop	Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( p = r -> ( p .no q ) = ( r .no q ) ) : No typesetting found for |- ( p = r -> ( p .no q ) = ( r .no q ) ) with typecode |-
2	1	eleq1d	Could not format ( p = r -> ( ( p .no q ) e. On <-> ( r .no q ) e. On ) ) : No typesetting found for |- ( p = r -> ( ( p .no q ) e. On <-> ( r .no q ) e. On ) ) with typecode |-
3		oveq1	Could not format ( p = r -> ( p .no b ) = ( r .no b ) ) : No typesetting found for |- ( p = r -> ( p .no b ) = ( r .no b ) ) with typecode |-
4	3	oveq2d	Could not format ( p = r -> ( ( a .no q ) +no ( p .no b ) ) = ( ( a .no q ) +no ( r .no b ) ) ) : No typesetting found for |- ( p = r -> ( ( a .no q ) +no ( p .no b ) ) = ( ( a .no q ) +no ( r .no b ) ) ) with typecode |-
5	4	eleq1d	Could not format ( p = r -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = r -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
6	5	ralbidv	Could not format ( p = r -> ( A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = r -> ( A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
7	6	raleqbi1dv	Could not format ( p = r -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = r -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
8	7	rabbidv	Could not format ( p = r -> { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( p = r -> { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
9	8	inteqd	Could not format ( p = r -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( p = r -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
10	1 9	eqeq12d	Could not format ( p = r -> ( ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) : No typesetting found for |- ( p = r -> ( ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-
11	2 10	anbi12d	Could not format ( p = r -> ( ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) : No typesetting found for |- ( p = r -> ( ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) with typecode |-
12		oveq2	Could not format ( q = s -> ( r .no q ) = ( r .no s ) ) : No typesetting found for |- ( q = s -> ( r .no q ) = ( r .no s ) ) with typecode |-
13	12	eleq1d	Could not format ( q = s -> ( ( r .no q ) e. On <-> ( r .no s ) e. On ) ) : No typesetting found for |- ( q = s -> ( ( r .no q ) e. On <-> ( r .no s ) e. On ) ) with typecode |-
14		oveq2	Could not format ( q = s -> ( a .no q ) = ( a .no s ) ) : No typesetting found for |- ( q = s -> ( a .no q ) = ( a .no s ) ) with typecode |-
15	14	oveq1d	Could not format ( q = s -> ( ( a .no q ) +no ( r .no b ) ) = ( ( a .no s ) +no ( r .no b ) ) ) : No typesetting found for |- ( q = s -> ( ( a .no q ) +no ( r .no b ) ) = ( ( a .no s ) +no ( r .no b ) ) ) with typecode |-
16	15	eleq1d	Could not format ( q = s -> ( ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( q = s -> ( ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
17	16	raleqbi1dv	Could not format ( q = s -> ( A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( q = s -> ( A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
18	17	ralbidv	Could not format ( q = s -> ( A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( q = s -> ( A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
19	18	rabbidv	Could not format ( q = s -> { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( q = s -> { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
20	19	inteqd	Could not format ( q = s -> |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( q = s -> |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
21	12 20	eqeq12d	Could not format ( q = s -> ( ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) : No typesetting found for |- ( q = s -> ( ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-
22	13 21	anbi12d	Could not format ( q = s -> ( ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) : No typesetting found for |- ( q = s -> ( ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) with typecode |-
23		oveq1	Could not format ( p = r -> ( p .no s ) = ( r .no s ) ) : No typesetting found for |- ( p = r -> ( p .no s ) = ( r .no s ) ) with typecode |-
24	23	eleq1d	Could not format ( p = r -> ( ( p .no s ) e. On <-> ( r .no s ) e. On ) ) : No typesetting found for |- ( p = r -> ( ( p .no s ) e. On <-> ( r .no s ) e. On ) ) with typecode |-
25	3	oveq2d	Could not format ( p = r -> ( ( a .no s ) +no ( p .no b ) ) = ( ( a .no s ) +no ( r .no b ) ) ) : No typesetting found for |- ( p = r -> ( ( a .no s ) +no ( p .no b ) ) = ( ( a .no s ) +no ( r .no b ) ) ) with typecode |-
26	25	eleq1d	Could not format ( p = r -> ( ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = r -> ( ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
27	26	ralbidv	Could not format ( p = r -> ( A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = r -> ( A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
28	27	raleqbi1dv	Could not format ( p = r -> ( A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = r -> ( A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
29	28	rabbidv	Could not format ( p = r -> { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( p = r -> { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
30	29	inteqd	Could not format ( p = r -> |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( p = r -> |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
31	23 30	eqeq12d	Could not format ( p = r -> ( ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) : No typesetting found for |- ( p = r -> ( ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-
32	24 31	anbi12d	Could not format ( p = r -> ( ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) : No typesetting found for |- ( p = r -> ( ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) with typecode |-
33		oveq1	Could not format ( p = A -> ( p .no q ) = ( A .no q ) ) : No typesetting found for |- ( p = A -> ( p .no q ) = ( A .no q ) ) with typecode |-
34	33	eleq1d	Could not format ( p = A -> ( ( p .no q ) e. On <-> ( A .no q ) e. On ) ) : No typesetting found for |- ( p = A -> ( ( p .no q ) e. On <-> ( A .no q ) e. On ) ) with typecode |-
35		oveq1	Could not format ( p = A -> ( p .no b ) = ( A .no b ) ) : No typesetting found for |- ( p = A -> ( p .no b ) = ( A .no b ) ) with typecode |-
36	35	oveq2d	Could not format ( p = A -> ( ( a .no q ) +no ( p .no b ) ) = ( ( a .no q ) +no ( A .no b ) ) ) : No typesetting found for |- ( p = A -> ( ( a .no q ) +no ( p .no b ) ) = ( ( a .no q ) +no ( A .no b ) ) ) with typecode |-
37	36	eleq1d	Could not format ( p = A -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = A -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
38	37	ralbidv	Could not format ( p = A -> ( A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = A -> ( A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
39	38	raleqbi1dv	Could not format ( p = A -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( p = A -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
40	39	rabbidv	Could not format ( p = A -> { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( p = A -> { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
41	40	inteqd	Could not format ( p = A -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( p = A -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
42	33 41	eqeq12d	Could not format ( p = A -> ( ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) : No typesetting found for |- ( p = A -> ( ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-
43	34 42	anbi12d	Could not format ( p = A -> ( ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( A .no q ) e. On /\ ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) : No typesetting found for |- ( p = A -> ( ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( A .no q ) e. On /\ ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) with typecode |-
44		oveq2	Could not format ( q = B -> ( A .no q ) = ( A .no B ) ) : No typesetting found for |- ( q = B -> ( A .no q ) = ( A .no B ) ) with typecode |-
45	44	eleq1d	Could not format ( q = B -> ( ( A .no q ) e. On <-> ( A .no B ) e. On ) ) : No typesetting found for |- ( q = B -> ( ( A .no q ) e. On <-> ( A .no B ) e. On ) ) with typecode |-
46		oveq2	Could not format ( q = B -> ( a .no q ) = ( a .no B ) ) : No typesetting found for |- ( q = B -> ( a .no q ) = ( a .no B ) ) with typecode |-
47	46	oveq1d	Could not format ( q = B -> ( ( a .no q ) +no ( A .no b ) ) = ( ( a .no B ) +no ( A .no b ) ) ) : No typesetting found for |- ( q = B -> ( ( a .no q ) +no ( A .no b ) ) = ( ( a .no B ) +no ( A .no b ) ) ) with typecode |-
48	47	eleq1d	Could not format ( q = B -> ( ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( q = B -> ( ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
49	48	raleqbi1dv	Could not format ( q = B -> ( A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( q = B -> ( A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
50	49	ralbidv	Could not format ( q = B -> ( A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( q = B -> ( A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
51	50	rabbidv	Could not format ( q = B -> { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( q = B -> { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
52	51	inteqd	Could not format ( q = B -> |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( q = B -> |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
53	44 52	eqeq12d	Could not format ( q = B -> ( ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) : No typesetting found for |- ( q = B -> ( ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } <-> ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-
54	45 53	anbi12d	Could not format ( q = B -> ( ( ( A .no q ) e. On /\ ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) : No typesetting found for |- ( q = B -> ( ( ( A .no q ) e. On /\ ( A .no q ) = |^| { x e. On | A. a e. A A. b e. q ( ( a .no q ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) <-> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) with typecode |-
55		simpl	Could not format ( ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( r .no s ) e. On ) : No typesetting found for |- ( ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( r .no s ) e. On ) with typecode |-
56	55	2ralimi	Could not format ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. r e. p A. s e. q ( r .no s ) e. On ) : No typesetting found for |- ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. r e. p A. s e. q ( r .no s ) e. On ) with typecode |-
57		simpl	Could not format ( ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( r .no q ) e. On ) : No typesetting found for |- ( ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( r .no q ) e. On ) with typecode |-
58	57	ralimi	Could not format ( A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. r e. p ( r .no q ) e. On ) : No typesetting found for |- ( A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. r e. p ( r .no q ) e. On ) with typecode |-
59		simpl	Could not format ( ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( p .no s ) e. On ) : No typesetting found for |- ( ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) -> ( p .no s ) e. On ) with typecode |-
60	59	ralimi	Could not format ( A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. s e. q ( p .no s ) e. On ) : No typesetting found for |- ( A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) -> A. s e. q ( p .no s ) e. On ) with typecode |-
61	56 58 60	3anim123i	Could not format ( ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) -> ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) : No typesetting found for |- ( ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) -> ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) with typecode |-
62		df-nmul	Could not format .no = frecs ( { <. t , u >. | ( t e. ( On X. On ) /\ u e. ( On X. On ) /\ ( ( ( 1st ` t ) _E ( 1st ` u ) \/ ( 1st ` t ) = ( 1st ` u ) ) /\ ( ( 2nd ` t ) _E ( 2nd ` u ) \/ ( 2nd ` t ) = ( 2nd ` u ) ) /\ t =/= u ) ) } , ( On X. On ) , ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ) : No typesetting found for |- .no = frecs ( { <. t , u >. | ( t e. ( On X. On ) /\ u e. ( On X. On ) /\ ( ( ( 1st ` t ) _E ( 1st ` u ) \/ ( 1st ` t ) = ( 1st ` u ) ) /\ ( ( 2nd ` t ) _E ( 2nd ` u ) \/ ( 2nd ` t ) = ( 2nd ` u ) ) /\ t =/= u ) ) } , ( On X. On ) , ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ) with typecode |-
63	62	on2recsov	Could not format ( ( p e. On /\ q e. On ) -> ( p .no q ) = ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) ) : No typesetting found for |- ( ( p e. On /\ q e. On ) -> ( p .no q ) = ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) ) with typecode |-
64	63	adantr	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) = ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) = ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) ) with typecode |-
65		opex	$$⊢⟨p,q⟩\in \mathrm{V}$$
66		nmulfn	Could not format .no Fn ( On X. On ) : No typesetting found for |- .no Fn ( On X. On ) with typecode |-
67		fnfun	Could not format ( .no Fn ( On X. On ) -> Fun .no ) : No typesetting found for |- ( .no Fn ( On X. On ) -> Fun .no ) with typecode |-
68	66 67	ax-mp	Could not format Fun .no : No typesetting found for |- Fun .no with typecode |-
69		vex	$$⊢p\in \mathrm{V}$$
70	69	sucex	$$⊢\mathrm{suc}p\in \mathrm{V}$$
71		vex	$$⊢q\in \mathrm{V}$$
72	71	sucex	$$⊢\mathrm{suc}q\in \mathrm{V}$$
73	70 72	xpex	$$⊢\mathrm{suc}p\times \mathrm{suc}q\in \mathrm{V}$$
74	73	difexi	$$⊢\left(\mathrm{suc}p\times \mathrm{suc}q\right)\setminus \left\{⟨p,q⟩\right\}\in \mathrm{V}$$
75		resfunexg	Could not format ( ( Fun .no /\ ( ( suc p X. suc q ) \ { <. p , q >. } ) e. _V ) -> ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V ) : No typesetting found for |- ( ( Fun .no /\ ( ( suc p X. suc q ) \ { <. p , q >. } ) e. _V ) -> ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V ) with typecode |-
76	68 74 75	mp2an	Could not format ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V : No typesetting found for |- ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V with typecode |-
77		elelsuc	$$⊢a\in p\to a\in \mathrm{suc}p$$
78	77	adantr	$$⊢\left(a\in p\wedge b\in q\right)\to a\in \mathrm{suc}p$$
79	78	adantl	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to a\in \mathrm{suc}p$$
80	71	sucid	$$⊢q\in \mathrm{suc}q$$
81	80	a1i	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to q\in \mathrm{suc}q$$
82	79 81	opelxpd	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to ⟨a,q⟩\in \left(\mathrm{suc}p\times \mathrm{suc}q\right)$$
83		eloni	$$⊢p\in \mathrm{On}\to \mathrm{Ord}p$$
84		ordirr	$$⊢\mathrm{Ord}p\to \neg p\in p$$
85		elequ1	$$⊢a=p\to \left(a\in p\leftrightarrow p\in p\right)$$
86	85	notbid	$$⊢a=p\to \left(\neg a\in p\leftrightarrow \neg p\in p\right)$$
87	86	biimprcd	$$⊢\neg p\in p\to \left(a=p\to \neg a\in p\right)$$
88	87	con2d	$$⊢\neg p\in p\to \left(a\in p\to \neg a=p\right)$$
89	83 84 88	3syl	$$⊢p\in \mathrm{On}\to \left(a\in p\to \neg a=p\right)$$
90	89	imp	$$⊢\left(p\in \mathrm{On}\wedge a\in p\right)\to \neg a=p$$
91	90	ad2ant2r	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to \neg a=p$$
92	91	intnanrd	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to \neg \left(a=p\wedge q=q\right)$$
93		opex	$$⊢⟨a,q⟩\in \mathrm{V}$$
94	93	elsn	$$⊢⟨a,q⟩\in \left\{⟨p,q⟩\right\}\leftrightarrow ⟨a,q⟩=⟨p,q⟩$$
95		vex	$$⊢a\in \mathrm{V}$$
96	95 71	opth	$$⊢⟨a,q⟩=⟨p,q⟩\leftrightarrow \left(a=p\wedge q=q\right)$$
97	94 96	bitr2i	$$⊢\left(a=p\wedge q=q\right)\leftrightarrow ⟨a,q⟩\in \left\{⟨p,q⟩\right\}$$
98	92 97	sylnib	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to \neg ⟨a,q⟩\in \left\{⟨p,q⟩\right\}$$
99	82 98	eldifd	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to ⟨a,q⟩\in \left(\left(\mathrm{suc}p\times \mathrm{suc}q\right)\setminus \left\{⟨p,q⟩\right\}\right)$$
100	99	fvresd	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , q >. ) = ( .no ` <. a , q >. ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , q >. ) = ( .no ` <. a , q >. ) ) with typecode |-
101		df-ov	Could not format ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , q >. ) : No typesetting found for |- ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , q >. ) with typecode |-
102		df-ov	Could not format ( a .no q ) = ( .no ` <. a , q >. ) : No typesetting found for |- ( a .no q ) = ( .no ` <. a , q >. ) with typecode |-
103	100 101 102	3eqtr4g	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) = ( a .no q ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) = ( a .no q ) ) with typecode |-
104	69	sucid	$$⊢p\in \mathrm{suc}p$$
105	104	a1i	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to p\in \mathrm{suc}p$$
106		elelsuc	$$⊢b\in q\to b\in \mathrm{suc}q$$
107	106	adantl	$$⊢\left(a\in p\wedge b\in q\right)\to b\in \mathrm{suc}q$$
108	107	adantl	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to b\in \mathrm{suc}q$$
109	105 108	opelxpd	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to ⟨p,b⟩\in \left(\mathrm{suc}p\times \mathrm{suc}q\right)$$
110		eloni	$$⊢q\in \mathrm{On}\to \mathrm{Ord}q$$
111		ordirr	$$⊢\mathrm{Ord}q\to \neg q\in q$$
112		elequ1	$$⊢b=q\to \left(b\in q\leftrightarrow q\in q\right)$$
113	112	notbid	$$⊢b=q\to \left(\neg b\in q\leftrightarrow \neg q\in q\right)$$
114	113	biimprcd	$$⊢\neg q\in q\to \left(b=q\to \neg b\in q\right)$$
115	114	con2d	$$⊢\neg q\in q\to \left(b\in q\to \neg b=q\right)$$
116	110 111 115	3syl	$$⊢q\in \mathrm{On}\to \left(b\in q\to \neg b=q\right)$$
117	116	imp	$$⊢\left(q\in \mathrm{On}\wedge b\in q\right)\to \neg b=q$$
118	117	ad2ant2l	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to \neg b=q$$
119	118	intnand	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to \neg \left(p=p\wedge b=q\right)$$
120		opex	$$⊢⟨p,b⟩\in \mathrm{V}$$
121	120	elsn	$$⊢⟨p,b⟩\in \left\{⟨p,q⟩\right\}\leftrightarrow ⟨p,b⟩=⟨p,q⟩$$
122		vex	$$⊢b\in \mathrm{V}$$
123	69 122	opth	$$⊢⟨p,b⟩=⟨p,q⟩\leftrightarrow \left(p=p\wedge b=q\right)$$
124	121 123	bitr2i	$$⊢\left(p=p\wedge b=q\right)\leftrightarrow ⟨p,b⟩\in \left\{⟨p,q⟩\right\}$$
125	119 124	sylnib	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to \neg ⟨p,b⟩\in \left\{⟨p,q⟩\right\}$$
126	109 125	eldifd	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to ⟨p,b⟩\in \left(\left(\mathrm{suc}p\times \mathrm{suc}q\right)\setminus \left\{⟨p,q⟩\right\}\right)$$
127	126	fvresd	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. p , b >. ) = ( .no ` <. p , b >. ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. p , b >. ) = ( .no ` <. p , b >. ) ) with typecode |-
128		df-ov	Could not format ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. p , b >. ) : No typesetting found for |- ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. p , b >. ) with typecode |-
129		df-ov	Could not format ( p .no b ) = ( .no ` <. p , b >. ) : No typesetting found for |- ( p .no b ) = ( .no ` <. p , b >. ) with typecode |-
130	127 128 129	3eqtr4g	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( p .no b ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( p .no b ) ) with typecode |-
131	103 130	oveq12d	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) = ( ( a .no q ) +no ( p .no b ) ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) = ( ( a .no q ) +no ( p .no b ) ) ) with typecode |-
132		sssucid	$$⊢p\subseteq \mathrm{suc}p$$
133		sssucid	$$⊢q\subseteq \mathrm{suc}q$$
134		xpss12	$$⊢\left(p\subseteq \mathrm{suc}p\wedge q\subseteq \mathrm{suc}q\right)\to p\times q\subseteq \mathrm{suc}p\times \mathrm{suc}q$$
135	132 133 134	mp2an	$$⊢p\times q\subseteq \mathrm{suc}p\times \mathrm{suc}q$$
136		opelxpi	$$⊢\left(a\in p\wedge b\in q\right)\to ⟨a,b⟩\in \left(p\times q\right)$$
137	135 136	sselid	$$⊢\left(a\in p\wedge b\in q\right)\to ⟨a,b⟩\in \left(\mathrm{suc}p\times \mathrm{suc}q\right)$$
138	137	adantl	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to ⟨a,b⟩\in \left(\mathrm{suc}p\times \mathrm{suc}q\right)$$
139	118	intnand	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to \neg \left(a=p\wedge b=q\right)$$
140		opex	$$⊢⟨a,b⟩\in \mathrm{V}$$
141	140	elsn	$$⊢⟨a,b⟩\in \left\{⟨p,q⟩\right\}\leftrightarrow ⟨a,b⟩=⟨p,q⟩$$
142	95 122	opth	$$⊢⟨a,b⟩=⟨p,q⟩\leftrightarrow \left(a=p\wedge b=q\right)$$
143	141 142	bitr2i	$$⊢\left(a=p\wedge b=q\right)\leftrightarrow ⟨a,b⟩\in \left\{⟨p,q⟩\right\}$$
144	139 143	sylnib	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to \neg ⟨a,b⟩\in \left\{⟨p,q⟩\right\}$$
145	138 144	eldifd	$$⊢\left(\left(p\in \mathrm{On}\wedge q\in \mathrm{On}\right)\wedge \left(a\in p\wedge b\in q\right)\right)\to ⟨a,b⟩\in \left(\left(\mathrm{suc}p\times \mathrm{suc}q\right)\setminus \left\{⟨p,q⟩\right\}\right)$$
146	145	fvresd	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , b >. ) = ( .no ` <. a , b >. ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , b >. ) = ( .no ` <. a , b >. ) ) with typecode |-
147		df-ov	Could not format ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , b >. ) : No typesetting found for |- ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ` <. a , b >. ) with typecode |-
148		df-ov	Could not format ( a .no b ) = ( .no ` <. a , b >. ) : No typesetting found for |- ( a .no b ) = ( .no ` <. a , b >. ) with typecode |-
149	146 147 148	3eqtr4g	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( a .no b ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) = ( a .no b ) ) with typecode |-
150	149	oveq2d	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) = ( x +no ( a .no b ) ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) = ( x +no ( a .no b ) ) ) with typecode |-
151	131 150	eleq12d	Could not format ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( a e. p /\ b e. q ) ) -> ( ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
152	151	2ralbidva	Could not format ( ( p e. On /\ q e. On ) -> ( A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) <-> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) ) ) : No typesetting found for |- ( ( p e. On /\ q e. On ) -> ( A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) <-> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) ) ) with typecode |-
153	152	rabbidv	Could not format ( ( p e. On /\ q e. On ) -> { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( ( p e. On /\ q e. On ) -> { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
154	153	inteqd	Could not format ( ( p e. On /\ q e. On ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( ( p e. On /\ q e. On ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
155	154	adantr	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
156		oveq1	Could not format ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( x +no ( a .no b ) ) = ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) : No typesetting found for |- ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( x +no ( a .no b ) ) = ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) with typecode |-
157	156	eleq2d	Could not format ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) ) : No typesetting found for |- ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) ) with typecode |-
158	157	2ralbidv	Could not format ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) ) : No typesetting found for |- ( x = suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) ) with typecode |-
159		ovex	Could not format ( ( c .no q ) +no ( p .no d ) ) e. _V : No typesetting found for |- ( ( c .no q ) +no ( p .no d ) ) e. _V with typecode |-
160	71 159	iunex	Could not format U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. _V : No typesetting found for |- U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. _V with typecode |-
161	160	dfiun2	Could not format U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } : No typesetting found for |- U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } with typecode |-
162	159	dfiun2	Could not format U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } : No typesetting found for |- U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } with typecode |-
163		oveq1	Could not format ( r = c -> ( r .no q ) = ( c .no q ) ) : No typesetting found for |- ( r = c -> ( r .no q ) = ( c .no q ) ) with typecode |-
164	163	eleq1d	Could not format ( r = c -> ( ( r .no q ) e. On <-> ( c .no q ) e. On ) ) : No typesetting found for |- ( r = c -> ( ( r .no q ) e. On <-> ( c .no q ) e. On ) ) with typecode |-
165		simplr2	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> A. r e. p ( r .no q ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> A. r e. p ( r .no q ) e. On ) with typecode |-
166	165	adantr	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> A. r e. p ( r .no q ) e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> A. r e. p ( r .no q ) e. On ) with typecode |-
167		simplr	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> c e. p ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> c e. p ) with typecode |-
168	164 166 167	rspcdva	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( c .no q ) e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( c .no q ) e. On ) with typecode |-
169		oveq2	Could not format ( s = d -> ( p .no s ) = ( p .no d ) ) : No typesetting found for |- ( s = d -> ( p .no s ) = ( p .no d ) ) with typecode |-
170	169	eleq1d	Could not format ( s = d -> ( ( p .no s ) e. On <-> ( p .no d ) e. On ) ) : No typesetting found for |- ( s = d -> ( ( p .no s ) e. On <-> ( p .no d ) e. On ) ) with typecode |-
171		simplr3	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> A. s e. q ( p .no s ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> A. s e. q ( p .no s ) e. On ) with typecode |-
172	171	adantr	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> A. s e. q ( p .no s ) e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> A. s e. q ( p .no s ) e. On ) with typecode |-
173		simpr	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> d e. q ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> d e. q ) with typecode |-
174	170 172 173	rspcdva	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( p .no d ) e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( p .no d ) e. On ) with typecode |-
175	168 174	naddcld	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
176		eleq1	Could not format ( x = ( ( c .no q ) +no ( p .no d ) ) -> ( x e. On <-> ( ( c .no q ) +no ( p .no d ) ) e. On ) ) : No typesetting found for |- ( x = ( ( c .no q ) +no ( p .no d ) ) -> ( x e. On <-> ( ( c .no q ) +no ( p .no d ) ) e. On ) ) with typecode |-
177	175 176	syl5ibrcom	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) /\ d e. q ) -> ( x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) with typecode |-
178	177	rexlimdva	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> ( E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> ( E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) with typecode |-
179	178	abssdv	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On ) with typecode |-
180	71	abrexex	Could not format { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. _V : No typesetting found for |- { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. _V with typecode |-
181	180	ssonunii	Could not format ( { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On ) : No typesetting found for |- ( { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On ) with typecode |-
182	179 181	syl	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On ) with typecode |-
183	162 182	eqeltrid	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
184		eleq1	Could not format ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( x e. On <-> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) ) : No typesetting found for |- ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( x e. On <-> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) ) with typecode |-
185	183 184	syl5ibrcom	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ c e. p ) -> ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) with typecode |-
186	185	rexlimdva	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) with typecode |-
187	186	abssdv	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On ) with typecode |-
188	69	abrexex	Could not format { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. _V : No typesetting found for |- { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. _V with typecode |-
189	188	ssonunii	Could not format ( { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On ) : No typesetting found for |- ( { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On ) with typecode |-
190	187 189	syl	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On ) with typecode |-
191	161 190	eqeltrid	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
192		onsuc	Could not format ( U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
193	191 192	syl	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
194		simplr2	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. r e. p ( r .no q ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. r e. p ( r .no q ) e. On ) with typecode |-
195	164	rspccva	Could not format ( ( A. r e. p ( r .no q ) e. On /\ c e. p ) -> ( c .no q ) e. On ) : No typesetting found for |- ( ( A. r e. p ( r .no q ) e. On /\ c e. p ) -> ( c .no q ) e. On ) with typecode |-
196	194 195	sylan	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( c .no q ) e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( c .no q ) e. On ) with typecode |-
197	196	adantr	Could not format ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( c .no q ) e. On ) : No typesetting found for |- ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( c .no q ) e. On ) with typecode |-
198		simplr3	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. s e. q ( p .no s ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. s e. q ( p .no s ) e. On ) with typecode |-
199	198	adantr	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> A. s e. q ( p .no s ) e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> A. s e. q ( p .no s ) e. On ) with typecode |-
200	170	rspccva	Could not format ( ( A. s e. q ( p .no s ) e. On /\ d e. q ) -> ( p .no d ) e. On ) : No typesetting found for |- ( ( A. s e. q ( p .no s ) e. On /\ d e. q ) -> ( p .no d ) e. On ) with typecode |-
201	199 200	sylan	Could not format ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( p .no d ) e. On ) : No typesetting found for |- ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( p .no d ) e. On ) with typecode |-
202	197 201	naddcld	Could not format ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
203	202 176	syl5ibrcom	Could not format ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) : No typesetting found for |- ( ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) /\ d e. q ) -> ( x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) with typecode |-
204	203	rexlimdva	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) with typecode |-
205	204	abssdv	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } C_ On ) with typecode |-
206	205 181	syl	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> U. { x | E. d e. q x = ( ( c .no q ) +no ( p .no d ) ) } e. On ) with typecode |-
207	162 206	eqeltrid	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
208	207 184	syl5ibrcom	Could not format ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) : No typesetting found for |- ( ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) /\ c e. p ) -> ( x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) with typecode |-
209	208	rexlimdva	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> x e. On ) ) with typecode |-
210	209	abssdv	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } C_ On ) with typecode |-
211	210 189	syl	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> U. { x | E. c e. p x = U_ d e. q ( ( c .no q ) +no ( p .no d ) ) } e. On ) with typecode |-
212	161 211	eqeltrid	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
213	212 192	syl	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) with typecode |-
214		oveq1	Could not format ( r = a -> ( r .no s ) = ( a .no s ) ) : No typesetting found for |- ( r = a -> ( r .no s ) = ( a .no s ) ) with typecode |-
215	214	eleq1d	Could not format ( r = a -> ( ( r .no s ) e. On <-> ( a .no s ) e. On ) ) : No typesetting found for |- ( r = a -> ( ( r .no s ) e. On <-> ( a .no s ) e. On ) ) with typecode |-
216		oveq2	Could not format ( s = b -> ( a .no s ) = ( a .no b ) ) : No typesetting found for |- ( s = b -> ( a .no s ) = ( a .no b ) ) with typecode |-
217	216	eleq1d	Could not format ( s = b -> ( ( a .no s ) e. On <-> ( a .no b ) e. On ) ) : No typesetting found for |- ( s = b -> ( ( a .no s ) e. On <-> ( a .no b ) e. On ) ) with typecode |-
218		simplr1	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. r e. p A. s e. q ( r .no s ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> A. r e. p A. s e. q ( r .no s ) e. On ) with typecode |-
219		simprl	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> a e. p ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> a e. p ) with typecode |-
220		simprr	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> b e. q ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> b e. q ) with typecode |-
221	215 217 218 219 220	rspc2dv	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( a .no b ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( a .no b ) e. On ) with typecode |-
222		naddword1	Could not format ( ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On /\ ( a .no b ) e. On ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) C_ ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) : No typesetting found for |- ( ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On /\ ( a .no b ) e. On ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) C_ ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) with typecode |-
223	213 221 222	syl2anc	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) C_ ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) C_ ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) with typecode |-
224		oveq1	Could not format ( c = a -> ( c .no q ) = ( a .no q ) ) : No typesetting found for |- ( c = a -> ( c .no q ) = ( a .no q ) ) with typecode |-
225	224	oveq1d	Could not format ( c = a -> ( ( c .no q ) +no ( p .no d ) ) = ( ( a .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( c = a -> ( ( c .no q ) +no ( p .no d ) ) = ( ( a .no q ) +no ( p .no d ) ) ) with typecode |-
226	225	iuneq2d	Could not format ( c = a -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( c = a -> U_ d e. q ( ( c .no q ) +no ( p .no d ) ) = U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) with typecode |-
227	226	sseq2d	Could not format ( c = a -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) ) : No typesetting found for |- ( c = a -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) ) with typecode |-
228		oveq2	Could not format ( d = b -> ( p .no d ) = ( p .no b ) ) : No typesetting found for |- ( d = b -> ( p .no d ) = ( p .no b ) ) with typecode |-
229	228	oveq2d	Could not format ( d = b -> ( ( a .no q ) +no ( p .no d ) ) = ( ( a .no q ) +no ( p .no b ) ) ) : No typesetting found for |- ( d = b -> ( ( a .no q ) +no ( p .no d ) ) = ( ( a .no q ) +no ( p .no b ) ) ) with typecode |-
230	229	sseq2d	Could not format ( d = b -> ( ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no b ) ) ) ) : No typesetting found for |- ( d = b -> ( ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no b ) ) ) ) with typecode |-
231		ssidd	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no b ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no b ) ) ) with typecode |-
232	230 220 231	rspcedvdw	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> E. d e. q ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> E. d e. q ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) ) with typecode |-
233		ssiun	Could not format ( E. d e. q ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( E. d e. q ( ( a .no q ) +no ( p .no b ) ) C_ ( ( a .no q ) +no ( p .no d ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) with typecode |-
234	232 233	syl	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( a .no q ) +no ( p .no d ) ) ) with typecode |-
235	227 219 234	rspcedvdw	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> E. c e. p ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> E. c e. p ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) with typecode |-
236		ssiun	Could not format ( E. c e. p ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( E. c e. p ( ( a .no q ) +no ( p .no b ) ) C_ U_ d e. q ( ( c .no q ) +no ( p .no d ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) with typecode |-
237	235 236	syl	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) with typecode |-
238		simpr2	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. r e. p ( r .no q ) e. On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. r e. p ( r .no q ) e. On ) with typecode |-
239		simpl	$$⊢\left(a\in p\wedge b\in q\right)\to a\in p$$
240		oveq1	Could not format ( r = a -> ( r .no q ) = ( a .no q ) ) : No typesetting found for |- ( r = a -> ( r .no q ) = ( a .no q ) ) with typecode |-
241	240	eleq1d	Could not format ( r = a -> ( ( r .no q ) e. On <-> ( a .no q ) e. On ) ) : No typesetting found for |- ( r = a -> ( ( r .no q ) e. On <-> ( a .no q ) e. On ) ) with typecode |-
242	241	rspccva	Could not format ( ( A. r e. p ( r .no q ) e. On /\ a e. p ) -> ( a .no q ) e. On ) : No typesetting found for |- ( ( A. r e. p ( r .no q ) e. On /\ a e. p ) -> ( a .no q ) e. On ) with typecode |-
243	238 239 242	syl2an	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( a .no q ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( a .no q ) e. On ) with typecode |-
244		simpr3	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. s e. q ( p .no s ) e. On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. s e. q ( p .no s ) e. On ) with typecode |-
245		simpr	$$⊢\left(a\in p\wedge b\in q\right)\to b\in q$$
246		oveq2	Could not format ( s = b -> ( p .no s ) = ( p .no b ) ) : No typesetting found for |- ( s = b -> ( p .no s ) = ( p .no b ) ) with typecode |-
247	246	eleq1d	Could not format ( s = b -> ( ( p .no s ) e. On <-> ( p .no b ) e. On ) ) : No typesetting found for |- ( s = b -> ( ( p .no s ) e. On <-> ( p .no b ) e. On ) ) with typecode |-
248	247	rspccva	Could not format ( ( A. s e. q ( p .no s ) e. On /\ b e. q ) -> ( p .no b ) e. On ) : No typesetting found for |- ( ( A. s e. q ( p .no s ) e. On /\ b e. q ) -> ( p .no b ) e. On ) with typecode |-
249	244 245 248	syl2an	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( p .no b ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( p .no b ) e. On ) with typecode |-
250	243 249	naddcld	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. On ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. On ) with typecode |-
251		onsssuc	Could not format ( ( ( ( a .no q ) +no ( p .no b ) ) e. On /\ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) ) : No typesetting found for |- ( ( ( ( a .no q ) +no ( p .no b ) ) e. On /\ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) e. On ) -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) ) with typecode |-
252	250 212 251	syl2anc	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( ( a .no q ) +no ( p .no b ) ) C_ U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) <-> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) ) with typecode |-
253	237 252	mpbid	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) ) with typecode |-
254	223 253	sseldd	Could not format ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) : No typesetting found for |- ( ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) /\ ( a e. p /\ b e. q ) ) -> ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) with typecode |-
255	254	ralrimivva	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( suc U_ c e. p U_ d e. q ( ( c .no q ) +no ( p .no d ) ) +no ( a .no b ) ) ) with typecode |-
256	158 193 255	rspcedvdw	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> E. x e. On A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> E. x e. On A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) ) with typecode |-
257		onintrab2	Could not format ( E. x e. On A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } e. On ) : No typesetting found for |- ( E. x e. On A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) <-> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } e. On ) with typecode |-
258	256 257	sylib	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } e. On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } e. On ) with typecode |-
259	155 258	eqeltrd	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } e. On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } e. On ) with typecode |-
260	69 71	op1std	$$⊢v=⟨p,q⟩\to 1^{st}\left(v\right)=p$$
261	69 71	op2ndd	$$⊢v=⟨p,q⟩\to 2^{nd}\left(v\right)=q$$
262	261	csbeq1d	$$⊢v=⟨p,q⟩\to ⦋2^{nd}\left(v\right)/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}=⦋q/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
263	260 262	csbeq12dv	$$⊢v=⟨p,q⟩\to ⦋1^{st}\left(v\right)/c⦌⦋2^{nd}\left(v\right)/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}=⦋p/c⦌⦋q/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
264		oveq1	$$⊢c=p\to cwb=pwb$$
265	264	oveq2d	$$⊢c=p\to \left(awd\right)+\left(cwb\right)=\left(awd\right)+\left(pwb\right)$$
266	265	eleq1d	$$⊢c=p\to \left(\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\leftrightarrow \left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right)$$
267	266	ralbidv	$$⊢c=p\to \left(\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\leftrightarrow \forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right)$$
268	267	raleqbi1dv	$$⊢c=p\to \left(\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\leftrightarrow \forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right)$$
269	268	rabbidv	$$⊢c=p\to \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}=\left\{x\in \mathrm{On}|\forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
270	269	inteqd	$$⊢c=p\to \bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}=\bigcap \left\{x\in \mathrm{On}|\forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
271	270	csbeq2dv	$$⊢c=p\to ⦋q/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}=⦋q/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
272	69 271	csbie	$$⊢⦋p/c⦌⦋q/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}=⦋q/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
273		oveq2	$$⊢d=q\to awd=awq$$
274	273	oveq1d	$$⊢d=q\to \left(awd\right)+\left(pwb\right)=\left(awq\right)+\left(pwb\right)$$
275	274	eleq1d	$$⊢d=q\to \left(\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\leftrightarrow \left(awq\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right)$$
276	275	raleqbi1dv	$$⊢d=q\to \left(\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\leftrightarrow \forall b\in q\left(awq\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right)$$
277	276	ralbidv	$$⊢d=q\to \left(\forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\leftrightarrow \forall a\in p\forall b\in q\left(awq\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right)$$
278	277	rabbidv	$$⊢d=q\to \left\{x\in \mathrm{On}|\forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}=\left\{x\in \mathrm{On}|\forall a\in p\forall b\in q\left(awq\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
279	278	inteqd	$$⊢d=q\to \bigcap \left\{x\in \mathrm{On}|\forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}=\bigcap \left\{x\in \mathrm{On}|\forall a\in p\forall b\in q\left(awq\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
280	71 279	csbie	$$⊢⦋q/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in p\forall b\in d\left(awd\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}=\bigcap \left\{x\in \mathrm{On}|\forall a\in p\forall b\in q\left(awq\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
281	272 280	eqtri	$$⊢⦋p/c⦌⦋q/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}=\bigcap \left\{x\in \mathrm{On}|\forall a\in p\forall b\in q\left(awq\right)+\left(pwb\right)\in \left(x+\left(awb\right)\right)\right\}$$
282		oveq	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( a w q ) = ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( a w q ) = ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) ) with typecode |-
283		oveq	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( p w b ) = ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( p w b ) = ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) with typecode |-
284	282 283	oveq12d	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( ( a w q ) +no ( p w b ) ) = ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( ( a w q ) +no ( p w b ) ) = ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) with typecode |-
285		oveq	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( a w b ) = ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( a w b ) = ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) with typecode |-
286	285	oveq2d	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( x +no ( a w b ) ) = ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( x +no ( a w b ) ) = ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) with typecode |-
287	284 286	eleq12d	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) ) with typecode |-
288	287	2ralbidv	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> ( A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) <-> A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) ) ) with typecode |-
289	288	rabbidv	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) with typecode |-
290	289	inteqd	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> |^| { x e. On | A. a e. p A. b e. q ( ( a w q ) +no ( p w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) with typecode |-
291	281 290	eqtrid	Could not format ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> [_ p / c ]_ [_ q / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) : No typesetting found for |- ( w = ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) -> [_ p / c ]_ [_ q / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) with typecode |-
292		eqid	$$⊢\left(v\in \mathrm{V},w\in \mathrm{V}⟼⦋1^{st}\left(v\right)/c⦌⦋2^{nd}\left(v\right)/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}\right)=\left(v\in \mathrm{V},w\in \mathrm{V}⟼⦋1^{st}\left(v\right)/c⦌⦋2^{nd}\left(v\right)/d⦌\bigcap \left\{x\in \mathrm{On}|\forall a\in c\forall b\in d\left(awd\right)+\left(cwb\right)\in \left(x+\left(awb\right)\right)\right\}\right)$$
293	263 291 292	ovmpog	Could not format ( ( <. p , q >. e. _V /\ ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V /\ |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } e. On ) -> ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) : No typesetting found for |- ( ( <. p , q >. e. _V /\ ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) e. _V /\ |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } e. On ) -> ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) with typecode |-
294	65 76 259 293	mp3an12i	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( <. p , q >. ( v e. _V , w e. _V |-> [_ ( 1st ` v ) / c ]_ [_ ( 2nd ` v ) / d ]_ |^| { x e. On | A. a e. c A. b e. d ( ( a w d ) +no ( c w b ) ) e. ( x +no ( a w b ) ) } ) ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) ) = |^| { x e. On | A. a e. p A. b e. q ( ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) q ) +no ( p ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) e. ( x +no ( a ( .no |` ( ( suc p X. suc q ) \ { <. p , q >. } ) ) b ) ) } ) with typecode |-
295	64 294 155	3eqtrd	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) with typecode |-
296	295 258	eqeltrd	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) e. On ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( p .no q ) e. On ) with typecode |-
297	296 295	jca	Could not format ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) : No typesetting found for |- ( ( ( p e. On /\ q e. On ) /\ ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-
298	297	ex	Could not format ( ( p e. On /\ q e. On ) -> ( ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) : No typesetting found for |- ( ( p e. On /\ q e. On ) -> ( ( A. r e. p A. s e. q ( r .no s ) e. On /\ A. r e. p ( r .no q ) e. On /\ A. s e. q ( p .no s ) e. On ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) with typecode |-
299	61 298	syl5	Could not format ( ( p e. On /\ q e. On ) -> ( ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) : No typesetting found for |- ( ( p e. On /\ q e. On ) -> ( ( A. r e. p A. s e. q ( ( r .no s ) e. On /\ ( r .no s ) = |^| { x e. On | A. a e. r A. b e. s ( ( a .no s ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. r e. p ( ( r .no q ) e. On /\ ( r .no q ) = |^| { x e. On | A. a e. r A. b e. q ( ( a .no q ) +no ( r .no b ) ) e. ( x +no ( a .no b ) ) } ) /\ A. s e. q ( ( p .no s ) e. On /\ ( p .no s ) = |^| { x e. On | A. a e. p A. b e. s ( ( a .no s ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) -> ( ( p .no q ) e. On /\ ( p .no q ) = |^| { x e. On | A. a e. p A. b e. q ( ( a .no q ) +no ( p .no b ) ) e. ( x +no ( a .no b ) ) } ) ) ) with typecode |-
300	11 22 32 43 54 299	on2ind	Could not format ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( ( A .no B ) e. On /\ ( A .no B ) = |^| { x e. On | A. a e. A A. b e. B ( ( a .no B ) +no ( A .no b ) ) e. ( x +no ( a .no b ) ) } ) ) with typecode |-