Theorem naddgeoa

Description: Natural addition results in a value greater than or equal than that of ordinal addition. (Contributed by RP, 1-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢a=c\to a{+}_{𝑜}b=c{+}_{𝑜}b$$
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	1 2	sseq12d	Could not format ( a = c -> ( ( a +o b ) C_ ( a +no b ) <-> ( c +o b ) C_ ( c +no b ) ) ) : No typesetting found for |- ( a = c -> ( ( a +o b ) C_ ( a +no b ) <-> ( c +o b ) C_ ( c +no b ) ) ) with typecode |-
4		oveq2	$$⊢b=d\to c{+}_{𝑜}b=c{+}_{𝑜}d$$
5		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 |-
6	4 5	sseq12d	Could not format ( b = d -> ( ( c +o b ) C_ ( c +no b ) <-> ( c +o d ) C_ ( c +no d ) ) ) : No typesetting found for |- ( b = d -> ( ( c +o b ) C_ ( c +no b ) <-> ( c +o d ) C_ ( c +no d ) ) ) with typecode |-
7		oveq1	$$⊢a=c\to a{+}_{𝑜}d=c{+}_{𝑜}d$$
8		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 |-
9	7 8	sseq12d	Could not format ( a = c -> ( ( a +o d ) C_ ( a +no d ) <-> ( c +o d ) C_ ( c +no d ) ) ) : No typesetting found for |- ( a = c -> ( ( a +o d ) C_ ( a +no d ) <-> ( c +o d ) C_ ( c +no d ) ) ) with typecode |-
10		oveq1	$$⊢a=A\to a{+}_{𝑜}b=A{+}_{𝑜}b$$
11		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 |-
12	10 11	sseq12d	Could not format ( a = A -> ( ( a +o b ) C_ ( a +no b ) <-> ( A +o b ) C_ ( A +no b ) ) ) : No typesetting found for |- ( a = A -> ( ( a +o b ) C_ ( a +no b ) <-> ( A +o b ) C_ ( A +no b ) ) ) with typecode |-
13		oveq2	$$⊢b=B\to A{+}_{𝑜}b=A{+}_{𝑜}B$$
14		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 |-
15	13 14	sseq12d	Could not format ( b = B -> ( ( A +o b ) C_ ( A +no b ) <-> ( A +o B ) C_ ( A +no B ) ) ) : No typesetting found for |- ( b = B -> ( ( A +o b ) C_ ( A +no b ) <-> ( A +o B ) C_ ( A +no B ) ) ) with typecode |-
16		simplll	Could not format ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> a e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> a e. On ) with typecode |-
17		simpllr	Could not format ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> b e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> b e. On ) with typecode |-
18		simplr	Could not format ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> Lim b ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> Lim b ) with typecode |-
19	17 18	jca	Could not format ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( b e. On /\ Lim b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( b e. On /\ Lim b ) ) with typecode |-
20		oalim	$$⊢\left(a\in \mathrm{On}\wedge \left(b\in \mathrm{On}\wedge \mathrm{Lim}b\right)\right)\to a{+}_{𝑜}b=\bigcup _{d\in b}\left(a{+}_{𝑜}d\right)$$
21	16 19 20	syl2anc	Could not format ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = U_ d e. b ( a +o d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = U_ d e. b ( a +o d ) ) with typecode |-
22		simpl	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge \mathrm{Lim}b\right)\to \left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)$$
23		simp3	Could not format ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> A. d e. b ( a +o d ) C_ ( a +no d ) ) : No typesetting found for |- ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> A. d e. b ( a +o d ) C_ ( a +no d ) ) with typecode |-
24		simpr	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o d ) C_ ( a +no d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o d ) C_ ( a +no d ) ) with typecode |-
25		simpr	$$⊢\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\to b\in \mathrm{On}$$
26		onelss	$$⊢b\in \mathrm{On}\to \left(d\in b\to d\subseteq b\right)$$
27	25 26	syl	$$⊢\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\to \left(d\in b\to d\subseteq b\right)$$
28	27	imp	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge d\in b\right)\to d\subseteq b$$
29		simplr	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge d\in b\right)\to b\in \mathrm{On}$$
30		simpr	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge d\in b\right)\to d\in b$$
31		onelon	$$⊢\left(b\in \mathrm{On}\wedge d\in b\right)\to d\in \mathrm{On}$$
32	29 30 31	syl2anc	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge d\in b\right)\to d\in \mathrm{On}$$
33		simpll	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge d\in b\right)\to a\in \mathrm{On}$$
34		naddss2	Could not format ( ( d e. On /\ b e. On /\ a e. On ) -> ( d C_ b <-> ( a +no d ) C_ ( a +no b ) ) ) : No typesetting found for |- ( ( d e. On /\ b e. On /\ a e. On ) -> ( d C_ b <-> ( a +no d ) C_ ( a +no b ) ) ) with typecode |-
35	32 29 33 34	syl3anc	Could not format ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( d C_ b <-> ( a +no d ) C_ ( a +no b ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( d C_ b <-> ( a +no d ) C_ ( a +no b ) ) ) with typecode |-
36	28 35	mpbid	Could not format ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( a +no d ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( a +no d ) C_ ( a +no b ) ) with typecode |-
37	36	adantr	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +no d ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +no d ) C_ ( a +no b ) ) with typecode |-
38	24 37	sstrd	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o d ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o d ) C_ ( a +no b ) ) with typecode |-
39	38	ex	Could not format ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( ( a +o d ) C_ ( a +no d ) -> ( a +o d ) C_ ( a +no b ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( ( a +o d ) C_ ( a +no d ) -> ( a +o d ) C_ ( a +no b ) ) ) with typecode |-
40	39	ralimdva	Could not format ( ( a e. On /\ b e. On ) -> ( A. d e. b ( a +o d ) C_ ( a +no d ) -> A. d e. b ( a +o d ) C_ ( a +no b ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( A. d e. b ( a +o d ) C_ ( a +no d ) -> A. d e. b ( a +o d ) C_ ( a +no b ) ) ) with typecode |-
41	40	imp	Could not format ( ( ( a e. On /\ b e. On ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> A. d e. b ( a +o d ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> A. d e. b ( a +o d ) C_ ( a +no b ) ) with typecode |-
42		iunss	Could not format ( U_ d e. b ( a +o d ) C_ ( a +no b ) <-> A. d e. b ( a +o d ) C_ ( a +no b ) ) : No typesetting found for |- ( U_ d e. b ( a +o d ) C_ ( a +no b ) <-> A. d e. b ( a +o d ) C_ ( a +no b ) ) with typecode |-
43	41 42	sylibr	Could not format ( ( ( a e. On /\ b e. On ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> U_ d e. b ( a +o d ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> U_ d e. b ( a +o d ) C_ ( a +no b ) ) with typecode |-
44	22 23 43	syl2an	Could not format ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> U_ d e. b ( a +o d ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> U_ d e. b ( a +o d ) C_ ( a +no b ) ) with typecode |-
45	21 44	eqsstrd	Could not format ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ Lim b ) /\ ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) C_ ( a +no b ) ) with typecode |-
46	45	exp31	Could not format ( ( a e. On /\ b e. On ) -> ( Lim b -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( Lim b -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) with typecode |-
47		dflim3	$$⊢\mathrm{Lim}b\leftrightarrow \left(\mathrm{Ord}b\wedge \neg \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)$$
48	47	notbii	$$⊢\neg \mathrm{Lim}b\leftrightarrow \neg \left(\mathrm{Ord}b\wedge \neg \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)$$
49		iman	$$⊢\left(\mathrm{Ord}b\to \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)\leftrightarrow \neg \left(\mathrm{Ord}b\wedge \neg \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)$$
50	48 49	bitr4i	$$⊢\neg \mathrm{Lim}b\leftrightarrow \left(\mathrm{Ord}b\to \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)$$
51		eloni	$$⊢b\in \mathrm{On}\to \mathrm{Ord}b$$
52		pm5.5	$$⊢\mathrm{Ord}b\to \left(\left(\mathrm{Ord}b\to \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)\leftrightarrow \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)$$
53	25 51 52	3syl	$$⊢\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\to \left(\left(\mathrm{Ord}b\to \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)\leftrightarrow \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)$$
54	50 53	bitrid	$$⊢\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\to \left(\neg \mathrm{Lim}b\leftrightarrow \left(b=\varnothing \vee \exists d\in \mathrm{On}b=\mathrm{suc}d\right)\right)$$
55		ssidd	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge b=\varnothing \right)\to a\subseteq a$$
56		simpr	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge b=\varnothing \right)\to b=\varnothing$$
57	56	oveq2d	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge b=\varnothing \right)\to a{+}_{𝑜}b=a{+}_{𝑜}\varnothing$$
58		simpll	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge b=\varnothing \right)\to a\in \mathrm{On}$$
59		oa0	$$⊢a\in \mathrm{On}\to a{+}_{𝑜}\varnothing =a$$
60	58 59	syl	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge b=\varnothing \right)\to a{+}_{𝑜}\varnothing =a$$
61	57 60	eqtrd	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge b=\varnothing \right)\to a{+}_{𝑜}b=a$$
62	56	oveq2d	Could not format ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no b ) = ( a +no (/) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no b ) = ( a +no (/) ) ) with typecode |-
63		naddrid	Could not format ( a e. On -> ( a +no (/) ) = a ) : No typesetting found for |- ( a e. On -> ( a +no (/) ) = a ) with typecode |-
64	58 63	syl	Could not format ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no (/) ) = a ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no (/) ) = a ) with typecode |-
65	62 64	eqtrd	Could not format ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no b ) = a ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +no b ) = a ) with typecode |-
66	55 61 65	3sstr4d	Could not format ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +o b ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( a +o b ) C_ ( a +no b ) ) with typecode |-
67	66	a1d	Could not format ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ b = (/) ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) with typecode |-
68	67	ex	Could not format ( ( a e. On /\ b e. On ) -> ( b = (/) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( b = (/) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) with typecode |-
69		vex	$$⊢d\in \mathrm{V}$$
70	69	sucid	$$⊢d\in \mathrm{suc}d$$
71		simpr	$$⊢\left(d\in \mathrm{On}\wedge b=\mathrm{suc}d\right)\to b=\mathrm{suc}d$$
72	70 71	eleqtrrid	$$⊢\left(d\in \mathrm{On}\wedge b=\mathrm{suc}d\right)\to d\in b$$
73	72 71	jca	$$⊢\left(d\in \mathrm{On}\wedge b=\mathrm{suc}d\right)\to \left(d\in b\wedge b=\mathrm{suc}d\right)$$
74	73	a1i	$$⊢\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\to \left(\left(d\in \mathrm{On}\wedge b=\mathrm{suc}d\right)\to \left(d\in b\wedge b=\mathrm{suc}d\right)\right)$$
75	74	reximdv2	$$⊢\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\to \left(\exists d\in \mathrm{On}b=\mathrm{suc}d\to \exists d\in bb=\mathrm{suc}d\right)$$
76		r19.29r	Could not format ( ( E. d e. b b = suc d /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> E. d e. b ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) : No typesetting found for |- ( ( E. d e. b b = suc d /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> E. d e. b ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) with typecode |-
77		simprr	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o d ) C_ ( a +no d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o d ) C_ ( a +no d ) ) with typecode |-
78	33 32	jca	$$⊢\left(\left(a\in \mathrm{On}\wedge b\in \mathrm{On}\right)\wedge d\in b\right)\to \left(a\in \mathrm{On}\wedge d\in \mathrm{On}\right)$$
79		oacl	$$⊢\left(a\in \mathrm{On}\wedge d\in \mathrm{On}\right)\to a{+}_{𝑜}d\in \mathrm{On}$$
80		eloni	$$⊢a{+}_{𝑜}d\in \mathrm{On}\to \mathrm{Ord}\left(a{+}_{𝑜}d\right)$$
81	79 80	syl	$$⊢\left(a\in \mathrm{On}\wedge d\in \mathrm{On}\right)\to \mathrm{Ord}\left(a{+}_{𝑜}d\right)$$
82		naddcl	Could not format ( ( a e. On /\ d e. On ) -> ( a +no d ) e. On ) : No typesetting found for |- ( ( a e. On /\ d e. On ) -> ( a +no d ) e. On ) with typecode |-
83		eloni	Could not format ( ( a +no d ) e. On -> Ord ( a +no d ) ) : No typesetting found for |- ( ( a +no d ) e. On -> Ord ( a +no d ) ) with typecode |-
84	82 83	syl	Could not format ( ( a e. On /\ d e. On ) -> Ord ( a +no d ) ) : No typesetting found for |- ( ( a e. On /\ d e. On ) -> Ord ( a +no d ) ) with typecode |-
85	81 84	jca	Could not format ( ( a e. On /\ d e. On ) -> ( Ord ( a +o d ) /\ Ord ( a +no d ) ) ) : No typesetting found for |- ( ( a e. On /\ d e. On ) -> ( Ord ( a +o d ) /\ Ord ( a +no d ) ) ) with typecode |-
86		ordsucsssuc	Could not format ( ( Ord ( a +o d ) /\ Ord ( a +no d ) ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) ) : No typesetting found for |- ( ( Ord ( a +o d ) /\ Ord ( a +no d ) ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) ) with typecode |-
87	78 85 86	3syl	Could not format ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) ) : No typesetting found for |- ( ( ( a e. On /\ b e. On ) /\ d e. b ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) ) with typecode |-
88	87	adantr	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( ( a +o d ) C_ ( a +no d ) <-> suc ( a +o d ) C_ suc ( a +no d ) ) ) with typecode |-
89	77 88	mpbid	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> suc ( a +o d ) C_ suc ( a +no d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> suc ( a +o d ) C_ suc ( a +no d ) ) with typecode |-
90		simprl	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> b = suc d ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> b = suc d ) with typecode |-
91	90	oveq2d	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = ( a +o suc d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = ( a +o suc d ) ) with typecode |-
92	78	adantr	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a e. On /\ d e. On ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a e. On /\ d e. On ) ) with typecode |-
93		oasuc	$$⊢\left(a\in \mathrm{On}\wedge d\in \mathrm{On}\right)\to a{+}_{𝑜}\mathrm{suc}d=\mathrm{suc}\left(a{+}_{𝑜}d\right)$$
94	92 93	syl	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o suc d ) = suc ( a +o d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o suc d ) = suc ( a +o d ) ) with typecode |-
95	91 94	eqtrd	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = suc ( a +o d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) = suc ( a +o d ) ) with typecode |-
96	90	oveq2d	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no b ) = ( a +no suc d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no b ) = ( a +no suc d ) ) with typecode |-
97		simplll	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> a e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> a e. On ) with typecode |-
98	31	ad4ant23	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> d e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> d e. On ) with typecode |-
99		naddsuc2	Could not format ( ( a e. On /\ d e. On ) -> ( a +no suc d ) = suc ( a +no d ) ) : No typesetting found for |- ( ( a e. On /\ d e. On ) -> ( a +no suc d ) = suc ( a +no d ) ) with typecode |-
100	97 98 99	syl2anc	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no suc d ) = suc ( a +no d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no suc d ) = suc ( a +no d ) ) with typecode |-
101	96 100	eqtrd	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no b ) = suc ( a +no d ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +no b ) = suc ( a +no d ) ) with typecode |-
102	89 95 101	3sstr4d	Could not format ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) C_ ( a +no b ) ) : No typesetting found for |- ( ( ( ( a e. On /\ b e. On ) /\ d e. b ) /\ ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) ) -> ( a +o b ) C_ ( a +no b ) ) with typecode |-
103	102	rexlimdva2	Could not format ( ( a e. On /\ b e. On ) -> ( E. d e. b ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( E. d e. b ( b = suc d /\ ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) with typecode |-
104	76 103	syl5	Could not format ( ( a e. On /\ b e. On ) -> ( ( E. d e. b b = suc d /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( ( E. d e. b b = suc d /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) with typecode |-
105	104	expd	Could not format ( ( a e. On /\ b e. On ) -> ( E. d e. b b = suc d -> ( A. d e. b ( a +o d ) C_ ( a +no d ) -> ( a +o b ) C_ ( a +no b ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( E. d e. b b = suc d -> ( A. d e. b ( a +o d ) C_ ( a +no d ) -> ( a +o b ) C_ ( a +no b ) ) ) ) with typecode |-
106	23 105	syl7	Could not format ( ( a e. On /\ b e. On ) -> ( E. d e. b b = suc d -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( E. d e. b b = suc d -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) with typecode |-
107	75 106	syld	Could not format ( ( a e. On /\ b e. On ) -> ( E. d e. On b = suc d -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( E. d e. On b = suc d -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) with typecode |-
108	68 107	jaod	Could not format ( ( a e. On /\ b e. On ) -> ( ( b = (/) \/ E. d e. On b = suc d ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( ( b = (/) \/ E. d e. On b = suc d ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) with typecode |-
109	54 108	sylbid	Could not format ( ( a e. On /\ b e. On ) -> ( -. Lim b -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( -. Lim b -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) ) with typecode |-
110	46 109	pm2.61d	Could not format ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) : No typesetting found for |- ( ( a e. On /\ b e. On ) -> ( ( A. c e. a A. d e. b ( c +o d ) C_ ( c +no d ) /\ A. c e. a ( c +o b ) C_ ( c +no b ) /\ A. d e. b ( a +o d ) C_ ( a +no d ) ) -> ( a +o b ) C_ ( a +no b ) ) ) with typecode |-
111	3 6 9 12 15 110	on2ind	Could not format ( ( A e. On /\ B e. On ) -> ( A +o B ) C_ ( A +no B ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +o B ) C_ ( A +no B ) ) with typecode |-