Theorem naddsuc2

Description: Natural addition with successor. (Contributed by RP, 1-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( a = c -> ( a +no suc b ) = ( c +no suc b ) ) : No typesetting found for |- ( a = c -> ( a +no suc b ) = ( c +no suc b ) ) with typecode |-
2		oveq1	Could not format ( a = c -> ( a +no b ) = ( c +no b ) ) : No typesetting found for |- ( a = c -> ( a +no b ) = ( c +no b ) ) with typecode |-
3		suceq	Could not format ( ( a +no b ) = ( c +no b ) -> suc ( a +no b ) = suc ( c +no b ) ) : No typesetting found for |- ( ( a +no b ) = ( c +no b ) -> suc ( a +no b ) = suc ( c +no b ) ) with typecode |-
4	2 3	syl	Could not format ( a = c -> suc ( a +no b ) = suc ( c +no b ) ) : No typesetting found for |- ( a = c -> suc ( a +no b ) = suc ( c +no b ) ) with typecode |-
5	1 4	eqeq12d	Could not format ( a = c -> ( ( a +no suc b ) = suc ( a +no b ) <-> ( c +no suc b ) = suc ( c +no b ) ) ) : No typesetting found for |- ( a = c -> ( ( a +no suc b ) = suc ( a +no b ) <-> ( c +no suc b ) = suc ( c +no b ) ) ) with typecode |-
6		suceq	$$⊢b=d\to \mathrm{suc}b=\mathrm{suc}d$$
7	6	oveq2d	Could not format ( b = d -> ( c +no suc b ) = ( c +no suc d ) ) : No typesetting found for |- ( b = d -> ( c +no suc b ) = ( c +no suc d ) ) with typecode |-
8		oveq2	Could not format ( b = d -> ( c +no b ) = ( c +no d ) ) : No typesetting found for |- ( b = d -> ( c +no b ) = ( c +no d ) ) with typecode |-
9		suceq	Could not format ( ( c +no b ) = ( c +no d ) -> suc ( c +no b ) = suc ( c +no d ) ) : No typesetting found for |- ( ( c +no b ) = ( c +no d ) -> suc ( c +no b ) = suc ( c +no d ) ) with typecode |-
10	8 9	syl	Could not format ( b = d -> suc ( c +no b ) = suc ( c +no d ) ) : No typesetting found for |- ( b = d -> suc ( c +no b ) = suc ( c +no d ) ) with typecode |-
11	7 10	eqeq12d	Could not format ( b = d -> ( ( c +no suc b ) = suc ( c +no b ) <-> ( c +no suc d ) = suc ( c +no d ) ) ) : No typesetting found for |- ( b = d -> ( ( c +no suc b ) = suc ( c +no b ) <-> ( c +no suc d ) = suc ( c +no d ) ) ) with typecode |-
12		oveq1	Could not format ( a = c -> ( a +no suc d ) = ( c +no suc d ) ) : No typesetting found for |- ( a = c -> ( a +no suc d ) = ( c +no suc d ) ) with typecode |-
13		oveq1	Could not format ( a = c -> ( a +no d ) = ( c +no d ) ) : No typesetting found for |- ( a = c -> ( a +no d ) = ( c +no d ) ) with typecode |-
14		suceq	Could not format ( ( a +no d ) = ( c +no d ) -> suc ( a +no d ) = suc ( c +no d ) ) : No typesetting found for |- ( ( a +no d ) = ( c +no d ) -> suc ( a +no d ) = suc ( c +no d ) ) with typecode |-
15	13 14	syl	Could not format ( a = c -> suc ( a +no d ) = suc ( c +no d ) ) : No typesetting found for |- ( a = c -> suc ( a +no d ) = suc ( c +no d ) ) with typecode |-
16	12 15	eqeq12d	Could not format ( a = c -> ( ( a +no suc d ) = suc ( a +no d ) <-> ( c +no suc d ) = suc ( c +no d ) ) ) : No typesetting found for |- ( a = c -> ( ( a +no suc d ) = suc ( a +no d ) <-> ( c +no suc d ) = suc ( c +no d ) ) ) with typecode |-
17		oveq1	Could not format ( a = A -> ( a +no suc b ) = ( A +no suc b ) ) : No typesetting found for |- ( a = A -> ( a +no suc b ) = ( A +no suc b ) ) with typecode |-
18		oveq1	Could not format ( a = A -> ( a +no b ) = ( A +no b ) ) : No typesetting found for |- ( a = A -> ( a +no b ) = ( A +no b ) ) with typecode |-
19		suceq	Could not format ( ( a +no b ) = ( A +no b ) -> suc ( a +no b ) = suc ( A +no b ) ) : No typesetting found for |- ( ( a +no b ) = ( A +no b ) -> suc ( a +no b ) = suc ( A +no b ) ) with typecode |-
20	18 19	syl	Could not format ( a = A -> suc ( a +no b ) = suc ( A +no b ) ) : No typesetting found for |- ( a = A -> suc ( a +no b ) = suc ( A +no b ) ) with typecode |-
21	17 20	eqeq12d	Could not format ( a = A -> ( ( a +no suc b ) = suc ( a +no b ) <-> ( A +no suc b ) = suc ( A +no b ) ) ) : No typesetting found for |- ( a = A -> ( ( a +no suc b ) = suc ( a +no b ) <-> ( A +no suc b ) = suc ( A +no b ) ) ) with typecode |-
22		suceq	$$⊢b=B\to \mathrm{suc}b=\mathrm{suc}B$$
23	22	oveq2d	Could not format ( b = B -> ( A +no suc b ) = ( A +no suc B ) ) : No typesetting found for |- ( b = B -> ( A +no suc b ) = ( A +no suc B ) ) with typecode |-
24		oveq2	Could not format ( b = B -> ( A +no b ) = ( A +no B ) ) : No typesetting found for |- ( b = B -> ( A +no b ) = ( A +no B ) ) with typecode |-
25		suceq	Could not format ( ( A +no b ) = ( A +no B ) -> suc ( A +no b ) = suc ( A +no B ) ) : No typesetting found for |- ( ( A +no b ) = ( A +no B ) -> suc ( A +no b ) = suc ( A +no B ) ) with typecode |-
26	24 25	syl	Could not format ( b = B -> suc ( A +no b ) = suc ( A +no B ) ) : No typesetting found for |- ( b = B -> suc ( A +no b ) = suc ( A +no B ) ) with typecode |-
27	23 26	eqeq12d	Could not format ( b = B -> ( ( A +no suc b ) = suc ( A +no b ) <-> ( A +no suc B ) = suc ( A +no B ) ) ) : No typesetting found for |- ( b = B -> ( ( A +no suc b ) = suc ( A +no b ) <-> ( A +no suc B ) = suc ( A +no B ) ) ) with typecode |-
28		simp2	Could not format ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) ) : No typesetting found for |- ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) ) with typecode |-
29	28	a1i	Could not format ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) ) ) with typecode |-
30		df-suc	$$⊢\mathrm{suc}b=b\cup \left\{b\right\}$$
31	30	a1i	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> suc b = ( b u. { b } ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> suc b = ( b u. { b } ) ) with typecode |-
32	31	raleqdv	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. suc b ( a +no d ) e. x <-> A. d e. ( b u. { b } ) ( a +no d ) e. x ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. suc b ( a +no d ) e. x <-> A. d e. ( b u. { b } ) ( a +no d ) e. x ) ) with typecode |-
33		vex	$$⊢b\in \mathrm{V}$$
34	33	a1i	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> b e. _V ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> b e. _V ) with typecode |-
35		oveq2	Could not format ( d = b -> ( a +no d ) = ( a +no b ) ) : No typesetting found for |- ( d = b -> ( a +no d ) = ( a +no b ) ) with typecode |-
36	35	eleq1d	Could not format ( d = b -> ( ( a +no d ) e. x <-> ( a +no b ) e. x ) ) : No typesetting found for |- ( d = b -> ( ( a +no d ) e. x <-> ( a +no b ) e. x ) ) with typecode |-
37	36	ralunsn	Could not format ( b e. _V -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( A. d e. b ( a +no d ) e. x /\ ( a +no b ) e. x ) ) ) : No typesetting found for |- ( b e. _V -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( A. d e. b ( a +no d ) e. x /\ ( a +no b ) e. x ) ) ) with typecode |-
38	34 37	syl	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( A. d e. b ( a +no d ) e. x /\ ( a +no b ) e. x ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( A. d e. b ( a +no d ) e. x /\ ( a +no b ) e. x ) ) ) with typecode |-
39	38	biancomd	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. ( b u. { b } ) ( a +no d ) e. x <-> ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) ) ) with typecode |-
40	32 39	bitrd	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. suc b ( a +no d ) e. x <-> ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. d e. suc b ( a +no d ) e. x <-> ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) ) ) with typecode |-
41		nfv	$$⊢Ⅎc\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)$$
42		nfra1	Could not format F/ c A. c e. a ( c +no suc b ) = suc ( c +no b ) : No typesetting found for |- F/ c A. c e. a ( c +no suc b ) = suc ( c +no b ) with typecode |-
43	41 42	nfan	Could not format F/ c ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) : No typesetting found for |- F/ c ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) with typecode |-
44		nfv	$$⊢Ⅎcx\in \mathrm{On}$$
45	43 44	nfan	Could not format F/ c ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) : No typesetting found for |- F/ c ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) with typecode |-
46		simplr	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> A. c e. a ( c +no suc b ) = suc ( c +no b ) ) with typecode |-
47	46	r19.21bi	Could not format ( ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) /\ c e. a ) -> ( c +no suc b ) = suc ( c +no b ) ) : No typesetting found for |- ( ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) /\ c e. a ) -> ( c +no suc b ) = suc ( c +no b ) ) with typecode |-
48	47	eleq1d	Could not format ( ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) /\ c e. a ) -> ( ( c +no suc b ) e. x <-> suc ( c +no b ) e. x ) ) : No typesetting found for |- ( ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) /\ c e. a ) -> ( ( c +no suc b ) e. x <-> suc ( c +no b ) e. x ) ) with typecode |-
49	45 48	ralbida	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. c e. a ( c +no suc b ) e. x <-> A. c e. a suc ( c +no b ) e. x ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( A. c e. a ( c +no suc b ) e. x <-> A. c e. a suc ( c +no b ) e. x ) ) with typecode |-
50	40 49	anbi12d	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) <-> ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) <-> ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) ) ) with typecode |-
51		anass	Could not format ( ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) <-> ( ( a +no b ) e. x /\ ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) : No typesetting found for |- ( ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) <-> ( ( a +no b ) e. x /\ ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) with typecode |-
52		simpll3	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> x e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> x e. On ) with typecode |-
53		simpr	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> d e. b ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> d e. b ) with typecode |-
54		simpll2	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> b e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> b e. On ) with typecode |-
55		onelon	$$⊢\left(b\in \mathrm{On}\wedge d\in b\right)\to d\in \mathrm{On}$$
56	54 53 55	syl2anc	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> d e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> d e. On ) with typecode |-
57		simpll1	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> a e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> a e. On ) with typecode |-
58		naddel2	Could not format ( ( d e. On /\ b e. On /\ a e. On ) -> ( d e. b <-> ( a +no d ) e. ( a +no b ) ) ) : No typesetting found for |- ( ( d e. On /\ b e. On /\ a e. On ) -> ( d e. b <-> ( a +no d ) e. ( a +no b ) ) ) with typecode |-
59	56 54 57 58	syl3anc	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( d e. b <-> ( a +no d ) e. ( a +no b ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( d e. b <-> ( a +no d ) e. ( a +no b ) ) ) with typecode |-
60	53 59	mpbid	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no d ) e. ( a +no b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no d ) e. ( a +no b ) ) with typecode |-
61		simplr	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no b ) e. x ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no b ) e. x ) with typecode |-
62	60 61	jca	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( ( a +no d ) e. ( a +no b ) /\ ( a +no b ) e. x ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( ( a +no d ) e. ( a +no b ) /\ ( a +no b ) e. x ) ) with typecode |-
63		ontr1	Could not format ( x e. On -> ( ( ( a +no d ) e. ( a +no b ) /\ ( a +no b ) e. x ) -> ( a +no d ) e. x ) ) : No typesetting found for |- ( x e. On -> ( ( ( a +no d ) e. ( a +no b ) /\ ( a +no b ) e. x ) -> ( a +no d ) e. x ) ) with typecode |-
64	52 62 63	sylc	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no d ) e. x ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ d e. b ) -> ( a +no d ) e. x ) with typecode |-
65	64	ralrimiva	Could not format ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> A. d e. b ( a +no d ) e. x ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> A. d e. b ( a +no d ) e. x ) with typecode |-
66		simpll1	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> a e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> a e. On ) with typecode |-
67		simpr	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> c e. a ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> c e. a ) with typecode |-
68		onelon	$$⊢\left(a\in \mathrm{On}\wedge c\in a\right)\to c\in \mathrm{On}$$
69	66 67 68	syl2anc	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> c e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> c e. On ) with typecode |-
70		simpll2	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> b e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> b e. On ) with typecode |-
71	69 66 70	3jca	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c e. On /\ a e. On /\ b e. On ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c e. On /\ a e. On /\ b e. On ) ) with typecode |-
72		naddelim	Could not format ( ( c e. On /\ a e. On /\ b e. On ) -> ( c e. a -> ( c +no b ) e. ( a +no b ) ) ) : No typesetting found for |- ( ( c e. On /\ a e. On /\ b e. On ) -> ( c e. a -> ( c +no b ) e. ( a +no b ) ) ) with typecode |-
73	71 67 72	sylc	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c +no b ) e. ( a +no b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c +no b ) e. ( a +no b ) ) with typecode |-
74		simplr	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( a +no b ) e. x ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( a +no b ) e. x ) with typecode |-
75		elunii	Could not format ( ( ( c +no b ) e. ( a +no b ) /\ ( a +no b ) e. x ) -> ( c +no b ) e. U. x ) : No typesetting found for |- ( ( ( c +no b ) e. ( a +no b ) /\ ( a +no b ) e. x ) -> ( c +no b ) e. U. x ) with typecode |-
76	73 74 75	syl2anc	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c +no b ) e. U. x ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( c +no b ) e. U. x ) with typecode |-
77		simpll3	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> x e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> x e. On ) with typecode |-
78		eloni	$$⊢x\in \mathrm{On}\to \mathrm{Ord}x$$
79	77 78	syl	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> Ord x ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> Ord x ) with typecode |-
80		ordsucuniel	Could not format ( Ord x -> ( ( c +no b ) e. U. x <-> suc ( c +no b ) e. x ) ) : No typesetting found for |- ( Ord x -> ( ( c +no b ) e. U. x <-> suc ( c +no b ) e. x ) ) with typecode |-
81	79 80	syl	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( ( c +no b ) e. U. x <-> suc ( c +no b ) e. x ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> ( ( c +no b ) e. U. x <-> suc ( c +no b ) e. x ) ) with typecode |-
82	76 81	mpbid	Could not format ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> suc ( c +no b ) e. x ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) /\ c e. a ) -> suc ( c +no b ) e. x ) with typecode |-
83	82	ralrimiva	Could not format ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> A. c e. a suc ( c +no b ) e. x ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> A. c e. a suc ( c +no b ) e. x ) with typecode |-
84	65 83	jca	Could not format ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On /\ x e. On ) /\ ( a +no b ) e. x ) -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) with typecode |-
85	84	ex	Could not format ( ( a e. On /\ b e. On /\ x e. On ) -> ( ( a +no b ) e. x -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On /\ x e. On ) -> ( ( a +no b ) e. x -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) with typecode |-
86	85	ad4ant124	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( a +no b ) e. x -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( a +no b ) e. x -> ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) with typecode |-
87	86	pm4.71d	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( a +no b ) e. x <-> ( ( a +no b ) e. x /\ ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( a +no b ) e. x <-> ( ( a +no b ) e. x /\ ( A. d e. b ( a +no d ) e. x /\ A. c e. a suc ( c +no b ) e. x ) ) ) ) with typecode |-
88	51 87	bitr4id	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) <-> ( a +no b ) e. x ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( ( ( a +no b ) e. x /\ A. d e. b ( a +no d ) e. x ) /\ A. c e. a suc ( c +no b ) e. x ) <-> ( a +no b ) e. x ) ) with typecode |-
89	50 88	bitrd	Could not format ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) <-> ( a +no b ) e. x ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) /\ x e. On ) -> ( ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) <-> ( a +no b ) e. x ) ) with typecode |-
90	89	rabbidva	Could not format ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } = { x e. On | ( a +no b ) e. x } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } = { x e. On | ( a +no b ) e. x } ) with typecode |-
91	90	inteqd	Could not format ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } = |^| { x e. On | ( a +no b ) e. x } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } = |^| { x e. On | ( a +no b ) e. x } ) with typecode |-
92		onsuc	$$⊢b\in \mathrm{On}\to \mathrm{suc}b\in \mathrm{On}$$
93		naddov2	Could not format ( ( a e. On /\ suc b e. On ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } ) : No typesetting found for |- ( ( a e. On /\ suc b e. On ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } ) with typecode |-
94	92 93	sylan2	Could not format ( ( a e. On /\ b e. On ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } ) with typecode |-
95	94	adantr	Could not format ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> ( a +no suc b ) = |^| { x e. On | ( A. d e. suc b ( a +no d ) e. x /\ A. c e. a ( c +no suc b ) e. x ) } ) with typecode |-
96		naddcl	Could not format ( ( a e. On /\ b e. On ) -> ( a +no b ) e. On ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( a +no b ) e. On ) with typecode |-
97		onsucmin	Could not format ( ( a +no b ) e. On -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } ) : No typesetting found for |- ( ( a +no b ) e. On -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } ) with typecode |-
98	96 97	syl	Could not format ( ( a e. On /\ b e. On ) -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } ) with typecode |-
99	98	adantr	Could not format ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> suc ( a +no b ) = |^| { x e. On | ( a +no b ) e. x } ) with typecode |-
100	91 95 99	3eqtr4d	Could not format ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> ( a +no suc b ) = suc ( a +no b ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) ) -> ( a +no suc b ) = suc ( a +no b ) ) with typecode |-
101	100	ex	Could not format ( ( a e. On /\ b e. On ) -> ( A. c e. a ( c +no suc b ) = suc ( c +no b ) -> ( a +no suc b ) = suc ( a +no b ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( A. c e. a ( c +no suc b ) = suc ( c +no b ) -> ( a +no suc b ) = suc ( a +no b ) ) ) with typecode |-
102	29 101	syld	Could not format ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> ( a +no suc b ) = suc ( a +no b ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +no suc d ) = suc ( c +no d ) /\ A. c e. a ( c +no suc b ) = suc ( c +no b ) /\ A. d e. b ( a +no suc d ) = suc ( a +no d ) ) -> ( a +no suc b ) = suc ( a +no b ) ) ) with typecode |-
103	5 11 16 21 27 102	on2ind	Could not format ( ( A e. On /\ B e. On ) -> ( A +no suc B ) = suc ( A +no B ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no suc B ) = suc ( A +no B ) ) with typecode |-