Theorem n0scut

Description: A cut form for surreal naturals. (Contributed by Scott Fenton, 2-Apr-2025)

	Ref	Expression
Assertion	n0scut	Could not format assertion : No typesetting found for |- ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		id	Could not format ( y = 0s -> y = 0s ) : No typesetting found for |- ( y = 0s -> y = 0s ) with typecode |-
2		oveq1	Could not format ( y = 0s -> ( y -s 1s ) = ( 0s -s 1s ) ) : No typesetting found for |- ( y = 0s -> ( y -s 1s ) = ( 0s -s 1s ) ) with typecode |-
3	2	sneqd	Could not format ( y = 0s -> { ( y -s 1s ) } = { ( 0s -s 1s ) } ) : No typesetting found for |- ( y = 0s -> { ( y -s 1s ) } = { ( 0s -s 1s ) } ) with typecode |-
4	3	oveq1d	Could not format ( y = 0s -> ( { ( y -s 1s ) } |s (/) ) = ( { ( 0s -s 1s ) } |s (/) ) ) : No typesetting found for |- ( y = 0s -> ( { ( y -s 1s ) } |s (/) ) = ( { ( 0s -s 1s ) } |s (/) ) ) with typecode |-
5	1 4	eqeq12d	Could not format ( y = 0s -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> 0s = ( { ( 0s -s 1s ) } |s (/) ) ) ) : No typesetting found for |- ( y = 0s -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> 0s = ( { ( 0s -s 1s ) } |s (/) ) ) ) with typecode |-
6		id	$$⊢y=x\to y=x$$
7		oveq1	Could not format ( y = x -> ( y -s 1s ) = ( x -s 1s ) ) : No typesetting found for |- ( y = x -> ( y -s 1s ) = ( x -s 1s ) ) with typecode |-
8	7	sneqd	Could not format ( y = x -> { ( y -s 1s ) } = { ( x -s 1s ) } ) : No typesetting found for |- ( y = x -> { ( y -s 1s ) } = { ( x -s 1s ) } ) with typecode |-
9	8	oveq1d	Could not format ( y = x -> ( { ( y -s 1s ) } |s (/) ) = ( { ( x -s 1s ) } |s (/) ) ) : No typesetting found for |- ( y = x -> ( { ( y -s 1s ) } |s (/) ) = ( { ( x -s 1s ) } |s (/) ) ) with typecode |-
10	6 9	eqeq12d	Could not format ( y = x -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> x = ( { ( x -s 1s ) } |s (/) ) ) ) : No typesetting found for |- ( y = x -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> x = ( { ( x -s 1s ) } |s (/) ) ) ) with typecode |-
11		id	Could not format ( y = ( x +s 1s ) -> y = ( x +s 1s ) ) : No typesetting found for |- ( y = ( x +s 1s ) -> y = ( x +s 1s ) ) with typecode |-
12		oveq1	Could not format ( y = ( x +s 1s ) -> ( y -s 1s ) = ( ( x +s 1s ) -s 1s ) ) : No typesetting found for |- ( y = ( x +s 1s ) -> ( y -s 1s ) = ( ( x +s 1s ) -s 1s ) ) with typecode |-
13	12	sneqd	Could not format ( y = ( x +s 1s ) -> { ( y -s 1s ) } = { ( ( x +s 1s ) -s 1s ) } ) : No typesetting found for |- ( y = ( x +s 1s ) -> { ( y -s 1s ) } = { ( ( x +s 1s ) -s 1s ) } ) with typecode |-
14	13	oveq1d	Could not format ( y = ( x +s 1s ) -> ( { ( y -s 1s ) } |s (/) ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) : No typesetting found for |- ( y = ( x +s 1s ) -> ( { ( y -s 1s ) } |s (/) ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) with typecode |-
15	11 14	eqeq12d	Could not format ( y = ( x +s 1s ) -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) ) : No typesetting found for |- ( y = ( x +s 1s ) -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) ) with typecode |-
16		id	$$⊢y=A\to y=A$$
17		oveq1	Could not format ( y = A -> ( y -s 1s ) = ( A -s 1s ) ) : No typesetting found for |- ( y = A -> ( y -s 1s ) = ( A -s 1s ) ) with typecode |-
18	17	sneqd	Could not format ( y = A -> { ( y -s 1s ) } = { ( A -s 1s ) } ) : No typesetting found for |- ( y = A -> { ( y -s 1s ) } = { ( A -s 1s ) } ) with typecode |-
19	18	oveq1d	Could not format ( y = A -> ( { ( y -s 1s ) } |s (/) ) = ( { ( A -s 1s ) } |s (/) ) ) : No typesetting found for |- ( y = A -> ( { ( y -s 1s ) } |s (/) ) = ( { ( A -s 1s ) } |s (/) ) ) with typecode |-
20	16 19	eqeq12d	Could not format ( y = A -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> A = ( { ( A -s 1s ) } |s (/) ) ) ) : No typesetting found for |- ( y = A -> ( y = ( { ( y -s 1s ) } |s (/) ) <-> A = ( { ( A -s 1s ) } |s (/) ) ) ) with typecode |-
21		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
22		1sno	Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |-
23		subscl	Could not format ( ( 0s e. No /\ 1s e. No ) -> ( 0s -s 1s ) e. No ) : No typesetting found for |- ( ( 0s e. No /\ 1s e. No ) -> ( 0s -s 1s ) e. No ) with typecode |-
24	21 22 23	mp2an	Could not format ( 0s -s 1s ) e. No : No typesetting found for |- ( 0s -s 1s ) e. No with typecode |-
25	24	a1i	Could not format ( T. -> ( 0s -s 1s ) e. No ) : No typesetting found for |- ( T. -> ( 0s -s 1s ) e. No ) with typecode |-
26	21	a1i	Could not format ( T. -> 0s e. No ) : No typesetting found for |- ( T. -> 0s e. No ) with typecode |-
27		0slt1s	Could not format 0s
28		addslid	Could not format ( 1s e. No -> ( 0s +s 1s ) = 1s ) : No typesetting found for |- ( 1s e. No -> ( 0s +s 1s ) = 1s ) with typecode |-
29	22 28	ax-mp	Could not format ( 0s +s 1s ) = 1s : No typesetting found for |- ( 0s +s 1s ) = 1s with typecode |-
30	27 29	breqtrri	Could not format 0s
31	22	a1i	Could not format ( T. -> 1s e. No ) : No typesetting found for |- ( T. -> 1s e. No ) with typecode |-
32	26 31 26	sltsubaddd	Could not format ( T. -> ( ( 0s -s 1s ) 0s ( ( 0s -s 1s ) 0s
33	30 32	mpbiri	Could not format ( T. -> ( 0s -s 1s ) ( 0s -s 1s )
34	25 26 33	ssltsn	Could not format ( T. -> { ( 0s -s 1s ) } < { ( 0s -s 1s ) } <
35	21	elexi	Could not format 0s e. _V : No typesetting found for |- 0s e. _V with typecode |-
36	35	snelpw	Could not format ( 0s e. No <-> { 0s } e. ~P No ) : No typesetting found for |- ( 0s e. No <-> { 0s } e. ~P No ) with typecode |-
37	21 36	mpbi	Could not format { 0s } e. ~P No : No typesetting found for |- { 0s } e. ~P No with typecode |-
38		nulssgt	Could not format ( { 0s } e. ~P No -> { 0s } < { 0s } <
39	37 38	ax-mp	Could not format { 0s } <
40	39	a1i	Could not format ( T. -> { 0s } < { 0s } <
41	34 40	cuteq0	Could not format ( T. -> ( { ( 0s -s 1s ) } |s (/) ) = 0s ) : No typesetting found for |- ( T. -> ( { ( 0s -s 1s ) } |s (/) ) = 0s ) with typecode |-
42	41	mptru	Could not format ( { ( 0s -s 1s ) } |s (/) ) = 0s : No typesetting found for |- ( { ( 0s -s 1s ) } |s (/) ) = 0s with typecode |-
43	42	eqcomi	Could not format 0s = ( { ( 0s -s 1s ) } |s (/) ) : No typesetting found for |- 0s = ( { ( 0s -s 1s ) } |s (/) ) with typecode |-
44		ovex	Could not format ( x -s 1s ) e. _V : No typesetting found for |- ( x -s 1s ) e. _V with typecode |-
45		oveq1	Could not format ( b = ( x -s 1s ) -> ( b +s 1s ) = ( ( x -s 1s ) +s 1s ) ) : No typesetting found for |- ( b = ( x -s 1s ) -> ( b +s 1s ) = ( ( x -s 1s ) +s 1s ) ) with typecode |-
46	45	eqeq2d	Could not format ( b = ( x -s 1s ) -> ( a = ( b +s 1s ) <-> a = ( ( x -s 1s ) +s 1s ) ) ) : No typesetting found for |- ( b = ( x -s 1s ) -> ( a = ( b +s 1s ) <-> a = ( ( x -s 1s ) +s 1s ) ) ) with typecode |-
47	44 46	rexsn	Could not format ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = ( ( x -s 1s ) +s 1s ) ) : No typesetting found for |- ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = ( ( x -s 1s ) +s 1s ) ) with typecode |-
48		n0sno	Could not format ( x e. NN0_s -> x e. No ) : No typesetting found for |- ( x e. NN0_s -> x e. No ) with typecode |-
49		npcans	Could not format ( ( x e. No /\ 1s e. No ) -> ( ( x -s 1s ) +s 1s ) = x ) : No typesetting found for |- ( ( x e. No /\ 1s e. No ) -> ( ( x -s 1s ) +s 1s ) = x ) with typecode |-
50	48 22 49	sylancl	Could not format ( x e. NN0_s -> ( ( x -s 1s ) +s 1s ) = x ) : No typesetting found for |- ( x e. NN0_s -> ( ( x -s 1s ) +s 1s ) = x ) with typecode |-
51	50	adantr	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( x -s 1s ) +s 1s ) = x ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( x -s 1s ) +s 1s ) = x ) with typecode |-
52	51	eqeq2d	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( a = ( ( x -s 1s ) +s 1s ) <-> a = x ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( a = ( ( x -s 1s ) +s 1s ) <-> a = x ) ) with typecode |-
53	47 52	bitrid	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) ) with typecode |-
54	53	alrimiv	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> A. a ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> A. a ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) ) with typecode |-
55		absn	Could not format ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } = { x } <-> A. a ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) ) : No typesetting found for |- ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } = { x } <-> A. a ( E. b e. { ( x -s 1s ) } a = ( b +s 1s ) <-> a = x ) ) with typecode |-
56	54 55	sylibr	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } = { x } ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } = { x } ) with typecode |-
57		oveq2	Could not format ( b = 0s -> ( x +s b ) = ( x +s 0s ) ) : No typesetting found for |- ( b = 0s -> ( x +s b ) = ( x +s 0s ) ) with typecode |-
58	57	eqeq2d	Could not format ( b = 0s -> ( a = ( x +s b ) <-> a = ( x +s 0s ) ) ) : No typesetting found for |- ( b = 0s -> ( a = ( x +s b ) <-> a = ( x +s 0s ) ) ) with typecode |-
59	35 58	rexsn	Could not format ( E. b e. { 0s } a = ( x +s b ) <-> a = ( x +s 0s ) ) : No typesetting found for |- ( E. b e. { 0s } a = ( x +s b ) <-> a = ( x +s 0s ) ) with typecode |-
60	48	addsridd	Could not format ( x e. NN0_s -> ( x +s 0s ) = x ) : No typesetting found for |- ( x e. NN0_s -> ( x +s 0s ) = x ) with typecode |-
61	60	adantr	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 0s ) = x ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 0s ) = x ) with typecode |-
62	61	eqeq2d	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( a = ( x +s 0s ) <-> a = x ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( a = ( x +s 0s ) <-> a = x ) ) with typecode |-
63	59 62	bitrid	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) ) with typecode |-
64	63	alrimiv	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> A. a ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> A. a ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) ) with typecode |-
65		absn	Could not format ( { a | E. b e. { 0s } a = ( x +s b ) } = { x } <-> A. a ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) ) : No typesetting found for |- ( { a | E. b e. { 0s } a = ( x +s b ) } = { x } <-> A. a ( E. b e. { 0s } a = ( x +s b ) <-> a = x ) ) with typecode |-
66	64 65	sylibr	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { a | E. b e. { 0s } a = ( x +s b ) } = { x } ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { a | E. b e. { 0s } a = ( x +s b ) } = { x } ) with typecode |-
67	56 66	uneq12d	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) = ( { x } u. { x } ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) = ( { x } u. { x } ) ) with typecode |-
68		unidm	$$⊢\left\{x\right\}\cup \left\{x\right\}=\left\{x\right\}$$
69	67 68	eqtrdi	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) = { x } ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) = { x } ) with typecode |-
70		rex0	Could not format -. E. b e. (/) a = ( b +s 1s ) : No typesetting found for |- -. E. b e. (/) a = ( b +s 1s ) with typecode |-
71	70	abf	Could not format { a | E. b e. (/) a = ( b +s 1s ) } = (/) : No typesetting found for |- { a | E. b e. (/) a = ( b +s 1s ) } = (/) with typecode |-
72		rex0	Could not format -. E. b e. (/) a = ( x +s b ) : No typesetting found for |- -. E. b e. (/) a = ( x +s b ) with typecode |-
73	72	abf	Could not format { a | E. b e. (/) a = ( x +s b ) } = (/) : No typesetting found for |- { a | E. b e. (/) a = ( x +s b ) } = (/) with typecode |-
74	71 73	uneq12i	Could not format ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = ( (/) u. (/) ) : No typesetting found for |- ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = ( (/) u. (/) ) with typecode |-
75		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
76	74 75	eqtri	Could not format ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = (/) : No typesetting found for |- ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = (/) with typecode |-
77	76	a1i	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = (/) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) = (/) ) with typecode |-
78	69 77	oveq12d	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) |s ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) ) = ( { x } |s (/) ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) |s ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) ) = ( { x } |s (/) ) ) with typecode |-
79		subscl	Could not format ( ( x e. No /\ 1s e. No ) -> ( x -s 1s ) e. No ) : No typesetting found for |- ( ( x e. No /\ 1s e. No ) -> ( x -s 1s ) e. No ) with typecode |-
80	48 22 79	sylancl	Could not format ( x e. NN0_s -> ( x -s 1s ) e. No ) : No typesetting found for |- ( x e. NN0_s -> ( x -s 1s ) e. No ) with typecode |-
81	80	adantr	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x -s 1s ) e. No ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x -s 1s ) e. No ) with typecode |-
82	44	snelpw	Could not format ( ( x -s 1s ) e. No <-> { ( x -s 1s ) } e. ~P No ) : No typesetting found for |- ( ( x -s 1s ) e. No <-> { ( x -s 1s ) } e. ~P No ) with typecode |-
83	81 82	sylib	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( x -s 1s ) } e. ~P No ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( x -s 1s ) } e. ~P No ) with typecode |-
84		nulssgt	Could not format ( { ( x -s 1s ) } e. ~P No -> { ( x -s 1s ) } < { ( x -s 1s ) } <
85	83 84	syl	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( x -s 1s ) } < { ( x -s 1s ) } <
86	39	a1i	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { 0s } < { 0s } <
87		simpr	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> x = ( { ( x -s 1s ) } |s (/) ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> x = ( { ( x -s 1s ) } |s (/) ) ) with typecode |-
88		df-1s	Could not format 1s = ( { 0s } |s (/) ) : No typesetting found for |- 1s = ( { 0s } |s (/) ) with typecode |-
89	88	a1i	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> 1s = ( { 0s } |s (/) ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> 1s = ( { 0s } |s (/) ) ) with typecode |-
90	85 86 87 89	addsunif	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 1s ) = ( ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) |s ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 1s ) = ( ( { a | E. b e. { ( x -s 1s ) } a = ( b +s 1s ) } u. { a | E. b e. { 0s } a = ( x +s b ) } ) |s ( { a | E. b e. (/) a = ( b +s 1s ) } u. { a | E. b e. (/) a = ( x +s b ) } ) ) ) with typecode |-
91	48	adantr	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> x e. No ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> x e. No ) with typecode |-
92		pncans	Could not format ( ( x e. No /\ 1s e. No ) -> ( ( x +s 1s ) -s 1s ) = x ) : No typesetting found for |- ( ( x e. No /\ 1s e. No ) -> ( ( x +s 1s ) -s 1s ) = x ) with typecode |-
93	91 22 92	sylancl	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( x +s 1s ) -s 1s ) = x ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( ( x +s 1s ) -s 1s ) = x ) with typecode |-
94	93	sneqd	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( ( x +s 1s ) -s 1s ) } = { x } ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> { ( ( x +s 1s ) -s 1s ) } = { x } ) with typecode |-
95	94	oveq1d	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) = ( { x } |s (/) ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) = ( { x } |s (/) ) ) with typecode |-
96	78 90 95	3eqtr4d	Could not format ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) : No typesetting found for |- ( ( x e. NN0_s /\ x = ( { ( x -s 1s ) } |s (/) ) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) with typecode |-
97	96	ex	Could not format ( x e. NN0_s -> ( x = ( { ( x -s 1s ) } |s (/) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) ) : No typesetting found for |- ( x e. NN0_s -> ( x = ( { ( x -s 1s ) } |s (/) ) -> ( x +s 1s ) = ( { ( ( x +s 1s ) -s 1s ) } |s (/) ) ) ) with typecode |-
98	5 10 15 20 43 97	n0sind	Could not format ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) ) : No typesetting found for |- ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) ) with typecode |-