Theorem nohalf

Description: An explicit expression for one half. This theorem avoids the axiom of infinity. (Contributed by Scott Fenton, 23-Jul-2025)

	Ref	Expression
Assertion	nohalf	Could not format assertion : No typesetting found for |- ( 1s /su 2s ) = ( { 0s } |s { 1s } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		snex	$$⊢\left\{0_s\right\}\in \mathrm{V}$$
2	1	a1i	$$⊢\top \to \left\{0_s\right\}\in \mathrm{V}$$
3		snex	$$⊢\left\{1_s\right\}\in \mathrm{V}$$
4	3	a1i	$$⊢\top \to \left\{1_s\right\}\in \mathrm{V}$$
5		0sno	$$⊢0_s\in \mathrm{No}$$
6	5	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
7	6	snssd	$$⊢\top \to \left\{0_s\right\}\subseteq \mathrm{No}$$
8		1sno	$$⊢1_s\in \mathrm{No}$$
9		snssi	$$⊢1_s\in \mathrm{No}\to \left\{1_s\right\}\subseteq \mathrm{No}$$
10	8 9	mp1i	$$⊢\top \to \left\{1_s\right\}\subseteq \mathrm{No}$$
11		velsn	$$⊢x\in \left\{0_s\right\}\leftrightarrow x=0_s$$
12		velsn	$$⊢y\in \left\{1_s\right\}\leftrightarrow y=1_s$$
13		0slt1s	$$⊢0_s{<}_s{1}_s$$
14		breq12	$$⊢\left(x=0_s\wedge y=1_s\right)\to \left(x{<}_{s}y\leftrightarrow 0_s{<}_s{1}_s\right)$$
15	13 14	mpbiri	$$⊢\left(x=0_s\wedge y=1_s\right)\to x{<}_{s}y$$
16	11 12 15	syl2anb	$$⊢\left(x\in \left\{0_s\right\}\wedge y\in \left\{1_s\right\}\right)\to x{<}_{s}y$$
17	16	3adant1	$$⊢\left(\top \wedge x\in \left\{0_s\right\}\wedge y\in \left\{1_s\right\}\right)\to x{<}_{s}y$$
18	2 4 7 10 17	ssltd	$$⊢\top \to \left\{0_s\right\}{\ll }_s\left\{1_s\right\}$$
19	18	scutcld	$$⊢\top \to \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
20	19	mptru	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
21		no2times	Could not format ( ( { 0s } |s { 1s } ) e. No -> ( 2s x.s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) ) : No typesetting found for |- ( ( { 0s } |s { 1s } ) e. No -> ( 2s x.s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) ) with typecode |-
22	20 21	ax-mp	Could not format ( 2s x.s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) : No typesetting found for |- ( 2s x.s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) with typecode |-
23		eqidd	$$⊢\top \to \left\{0_s\right\}{|}_s\left\{1_s\right\}=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
24	18 18 23 23	addsunif	$$⊢\top \to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=\left(\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}\right)$$
25	24	mptru	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=\left(\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}\right)$$
26	5	elexi	$$⊢0_s\in \mathrm{V}$$
27		oveq1	$$⊢y=0_s\to y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=0_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
28		addslid	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}\to 0_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
29	20 28	ax-mp	$$⊢0_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
30	27 29	eqtrdi	$$⊢y=0_s\to y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
31	30	eqeq2d	$$⊢y=0_s\to \left(x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
32	26 31	rexsn	$$⊢\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
33	32	abbii	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{x|x=\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
34		df-sn	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}=\left\{x|x=\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
35	33 34	eqtr4i	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
36		oveq2	$$⊢y=0_s\to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{0}_s$$
37		addsrid	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}\to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{0}_s=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
38	20 37	ax-mp	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{0}_s=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
39	36 38	eqtrdi	$$⊢y=0_s\to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
40	39	eqeq2d	$$⊢y=0_s\to \left(x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\leftrightarrow x=\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
41	26 40	rexsn	$$⊢\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\leftrightarrow x=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
42	41	abbii	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}=\left\{x|x=\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
43	42 34	eqtr4i	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
44	35 43	uneq12i	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\cup \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
45		unidm	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\cup \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
46	44 45	eqtri	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
47	8	elexi	$$⊢1_s\in \mathrm{V}$$
48		oveq1	$$⊢y=1_s\to y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
49		addscom	$$⊢\left(1_s\in \mathrm{No}\wedge \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}\right)\to 1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s$$
50	8 20 49	mp2an	$$⊢1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s$$
51	48 50	eqtrdi	$$⊢y=1_s\to y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s$$
52	51	eqeq2d	$$⊢y=1_s\to \left(x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
53	47 52	rexsn	$$⊢\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s$$
54	53	abbii	$$⊢\left\{x|\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{x|x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
55		df-sn	$$⊢\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=\left\{x|x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
56	54 55	eqtr4i	$$⊢\left\{x|\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
57		oveq2	$$⊢y=1_s\to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s$$
58	57	eqeq2d	$$⊢y=1_s\to \left(x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\leftrightarrow x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
59	47 58	rexsn	$$⊢\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\leftrightarrow x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s$$
60	59	abbii	$$⊢\left\{x|\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}=\left\{x|x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
61	60 55	eqtr4i	$$⊢\left\{x|\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}=\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
62	56 61	uneq12i	$$⊢\left\{x|\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}=\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\cup \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
63		unidm	$$⊢\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\cup \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
64	62 63	eqtri	$$⊢\left\{x|\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}=\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
65	46 64	oveq12i	$$⊢\left(\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}\right)=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
66		ral0	$$⊢\forall x\in \varnothing \left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right){<}_{s}x$$
67		slerflex	$$⊢1_s\in \mathrm{No}\to 1_s{\le }_s{1}_s$$
68	8 67	ax-mp	$$⊢1_s{\le }_s{1}_s$$
69		breq1	$$⊢y=1_s\to \left(y{\le }_s{1}_s\leftrightarrow 1_s{\le }_s{1}_s\right)$$
70	47 69	rexsn	$$⊢\exists y\in \left\{1_s\right\}y{\le }_s{1}_s\leftrightarrow 1_s{\le }_s{1}_s$$
71	68 70	mpbir	$$⊢\exists y\in \left\{1_s\right\}y{\le }_s{1}_s$$
72	71	olci	$$⊢\left(\exists x\in \left\{0_s\right\}\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){\le }_{s}x\vee \exists y\in \left\{1_s\right\}y{\le }_s{1}_s\right)$$
73	18	mptru	$$⊢\left\{0_s\right\}{\ll }_s\left\{1_s\right\}$$
74		snelpwi	$$⊢0_s\in \mathrm{No}\to \left\{0_s\right\}\in 𝒫\mathrm{No}$$
75	5 74	ax-mp	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}$$
76		nulssgt	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}\to \left\{0_s\right\}{\ll }_s\varnothing$$
77	75 76	ax-mp	$$⊢\left\{0_s\right\}{\ll }_s\varnothing$$
78		eqid	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
79		df-1s	$$⊢1_s=\left\{0_s\right\}{|}_s\varnothing$$
80		sltrec	$$⊢\left(\left(\left\{0_s\right\}{\ll }_s\left\{1_s\right\}\wedge \left\{0_s\right\}{\ll }_s\varnothing \right)\wedge \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}=\left\{0_s\right\}{|}_s\left\{1_s\right\}\wedge 1_s=\left\{0_s\right\}{|}_s\varnothing \right)\right)\to \left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s{1}_s\leftrightarrow \left(\exists x\in \left\{0_s\right\}\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){\le }_{s}x\vee \exists y\in \left\{1_s\right\}y{\le }_s{1}_s\right)\right)$$
81	73 77 78 79 80	mp4an	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s{1}_s\leftrightarrow \left(\exists x\in \left\{0_s\right\}\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){\le }_{s}x\vee \exists y\in \left\{1_s\right\}y{\le }_s{1}_s\right)$$
82	72 81	mpbir	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s{1}_s$$
83		ovex	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{V}$$
84		breq1	$$⊢y=\left\{0_s\right\}{|}_s\left\{1_s\right\}\to \left(y{<}_s{1}_s\leftrightarrow \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s{1}_s\right)$$
85	83 84	ralsn	$$⊢\forall y\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}y{<}_s{1}_s\leftrightarrow \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s{1}_s$$
86	82 85	mpbir	$$⊢\forall y\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}y{<}_s{1}_s$$
87		snex	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\in \mathrm{V}$$
88	87	a1i	$$⊢\top \to \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\in \mathrm{V}$$
89		snex	$$⊢\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\in \mathrm{V}$$
90	89	a1i	$$⊢\top \to \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\in \mathrm{V}$$
91	19	snssd	$$⊢\top \to \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\subseteq \mathrm{No}$$
92	8	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
93	19 92	addscld	$$⊢\top \to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\in \mathrm{No}$$
94	93	snssd	$$⊢\top \to \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\subseteq \mathrm{No}$$
95		velsn	$$⊢x\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\leftrightarrow x=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
96		velsn	$$⊢y\in \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\leftrightarrow y=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s$$
97		sltadd2	$$⊢\left(0_s\in \mathrm{No}\wedge 1_s\in \mathrm{No}\wedge \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}\right)\to \left(0_s{<}_s{1}_s\leftrightarrow \left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{0}_s\right){<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)\right)$$
98	5 8 20 97	mp3an	$$⊢0_s{<}_s{1}_s\leftrightarrow \left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{0}_s\right){<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
99	13 98	mpbi	$$⊢\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{0}_s\right){<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
100	38 99	eqbrtrri	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
101		breq12	$$⊢\left(x=\left\{0_s\right\}{|}_s\left\{1_s\right\}\wedge y=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)\to \left(x{<}_{s}y\leftrightarrow \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)\right)$$
102	100 101	mpbiri	$$⊢\left(x=\left\{0_s\right\}{|}_s\left\{1_s\right\}\wedge y=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)\to x{<}_{s}y$$
103	95 96 102	syl2anb	$$⊢\left(x\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\wedge y\in \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\to x{<}_{s}y$$
104	103	3adant1	$$⊢\left(\top \wedge x\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\wedge y\in \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\to x{<}_{s}y$$
105	88 90 91 94 104	ssltd	$$⊢\top \to \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
106	105	mptru	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
107		eqid	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}$$
108		slerec	$$⊢\left(\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\wedge \left\{0_s\right\}{\ll }_s\varnothing \right)\wedge \left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\wedge 1_s=\left\{0_s\right\}{|}_s\varnothing \right)\right)\to \left(\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right){\le }_s{1}_s\leftrightarrow \left(\forall x\in \varnothing \left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right){<}_{s}x\wedge \forall y\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}y{<}_s{1}_s\right)\right)$$
109	106 77 107 79 108	mp4an	$$⊢\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right){\le }_s{1}_s\leftrightarrow \left(\forall x\in \varnothing \left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right){<}_{s}x\wedge \forall y\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}y{<}_s{1}_s\right)$$
110	66 86 109	mpbir2an	$$⊢\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right){\le }_s{1}_s$$
111		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
112	8 111	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
113		slerflex	$$⊢0_s\in \mathrm{No}\to 0_s{\le }_s{0}_s$$
114	5 113	ax-mp	$$⊢0_s{\le }_s{0}_s$$
115		breq2	$$⊢x=0_s\to \left(0_s{\le }_{s}x\leftrightarrow 0_s{\le }_s{0}_s\right)$$
116	26 115	rexsn	$$⊢\exists x\in \left\{0_s\right\}{0}_s{\le }_{s}x\leftrightarrow 0_s{\le }_s{0}_s$$
117	114 116	mpbir	$$⊢\exists x\in \left\{0_s\right\}{0}_s{\le }_{s}x$$
118	117	orci	$$⊢\left(\exists x\in \left\{0_s\right\}{0}_s{\le }_{s}x\vee \exists y\in \varnothing y{\le }_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
119		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
120		nulssgt	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
121	119 120	ax-mp	$$⊢\varnothing {\ll }_s\varnothing$$
122		df-0s	$$⊢0_s=\varnothing {|}_s\varnothing$$
123		sltrec	$$⊢\left(\left(\varnothing {\ll }_s\varnothing \wedge \left\{0_s\right\}{\ll }_s\left\{1_s\right\}\right)\wedge \left(0_s=\varnothing {|}_s\varnothing \wedge \left\{0_s\right\}{|}_s\left\{1_s\right\}=\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)\to \left(0_s{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow \left(\exists x\in \left\{0_s\right\}{0}_s{\le }_{s}x\vee \exists y\in \varnothing y{\le }_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)\right)$$
124	121 73 122 78 123	mp4an	$$⊢0_s{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow \left(\exists x\in \left\{0_s\right\}{0}_s{\le }_{s}x\vee \exists y\in \varnothing y{\le }_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
125	118 124	mpbir	$$⊢0_s{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
126		sltadd1	$$⊢\left(0_s\in \mathrm{No}\wedge \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(0_s{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow \left(0_s{+}_s{1}_s\right){<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)\right)$$
127	5 20 8 126	mp3an	$$⊢0_s{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow \left(0_s{+}_s{1}_s\right){<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
128	125 127	mpbi	$$⊢\left(0_s{+}_s{1}_s\right){<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
129	112 128	eqbrtrri	$$⊢1_s{<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
130		ovex	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\in \mathrm{V}$$
131		breq2	$$⊢y=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\to \left(1_s{<}_{s}y\leftrightarrow 1_s{<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)\right)$$
132	130 131	ralsn	$$⊢\forall y\in \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}{1}_s{<}_{s}y\leftrightarrow 1_s{<}_s\left(\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right)$$
133	129 132	mpbir	$$⊢\forall y\in \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}{1}_s{<}_{s}y$$
134		breq2	$$⊢x=1_s\to \left(0_s{<}_{s}x\leftrightarrow 0_s{<}_s{1}_s\right)$$
135	47 134	ralsn	$$⊢\forall x\in \left\{1_s\right\}{0}_s{<}_{s}x\leftrightarrow 0_s{<}_s{1}_s$$
136	13 135	mpbir	$$⊢\forall x\in \left\{1_s\right\}{0}_s{<}_{s}x$$
137		ral0	$$⊢\forall y\in \varnothing y{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
138		slerec	$$⊢\left(\left(\varnothing {\ll }_s\varnothing \wedge \left\{0_s\right\}{\ll }_s\left\{1_s\right\}\right)\wedge \left(0_s=\varnothing {|}_s\varnothing \wedge \left\{0_s\right\}{|}_s\left\{1_s\right\}=\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)\to \left(0_s{\le }_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow \left(\forall x\in \left\{1_s\right\}{0}_s{<}_{s}x\wedge \forall y\in \varnothing y{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)\right)$$
139	121 73 122 78 138	mp4an	$$⊢0_s{\le }_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow \left(\forall x\in \left\{1_s\right\}{0}_s{<}_{s}x\wedge \forall y\in \varnothing y{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
140	136 137 139	mpbir2an	$$⊢0_s{\le }_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
141		breq2	$$⊢x=\left\{0_s\right\}{|}_s\left\{1_s\right\}\to \left(0_s{\le }_{s}x\leftrightarrow 0_s{\le }_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
142	83 141	rexsn	$$⊢\exists x\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{0}_s{\le }_{s}x\leftrightarrow 0_s{\le }_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
143	140 142	mpbir	$$⊢\exists x\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{0}_s{\le }_{s}x$$
144	143	orci	$$⊢\left(\exists x\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{0}_s{\le }_{s}x\vee \exists y\in \varnothing y{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)$$
145		sltrec	$$⊢\left(\left(\varnothing {\ll }_s\varnothing \wedge \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\wedge \left(0_s=\varnothing {|}_s\varnothing \wedge \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)\to \left(0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\leftrightarrow \left(\exists x\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{0}_s{\le }_{s}x\vee \exists y\in \varnothing y{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)\right)$$
146	121 106 122 107 145	mp4an	$$⊢0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\leftrightarrow \left(\exists x\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{0}_s{\le }_{s}x\vee \exists y\in \varnothing y{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)$$
147	144 146	mpbir	$$⊢0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)$$
148		breq1	$$⊢x=0_s\to \left(x{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\leftrightarrow 0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)$$
149	26 148	ralsn	$$⊢\forall x\in \left\{0_s\right\}x{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\leftrightarrow 0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)$$
150	147 149	mpbir	$$⊢\forall x\in \left\{0_s\right\}x{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)$$
151		slerec	$$⊢\left(\left(\left\{0_s\right\}{\ll }_s\varnothing \wedge \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\wedge \left(1_s=\left\{0_s\right\}{|}_s\varnothing \wedge \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)\to \left(1_s{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\leftrightarrow \left(\forall y\in \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}{1}_s{<}_{s}y\wedge \forall x\in \left\{0_s\right\}x{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)\right)$$
152	77 106 79 107 151	mp4an	$$⊢1_s{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\leftrightarrow \left(\forall y\in \left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}{1}_s{<}_{s}y\wedge \forall x\in \left\{0_s\right\}x{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)$$
153	133 150 152	mpbir2an	$$⊢1_s{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)$$
154	105	scutcld	$$⊢\top \to \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\in \mathrm{No}$$
155	154	mptru	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\in \mathrm{No}$$
156		sletri3	$$⊢\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=1_s\leftrightarrow \left(\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right){\le }_s{1}_s\wedge 1_s{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)\right)$$
157	155 8 156	mp2an	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=1_s\leftrightarrow \left(\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right){\le }_s{1}_s\wedge 1_s{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}\right)\right)$$
158	110 153 157	mpbir2an	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\right\}=1_s$$
159	65 158	eqtri	$$⊢\left(\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{x|\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\right\}\right)=1_s$$
160	25 159	eqtri	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)=1_s$$
161	22 160	eqtri	Could not format ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s : No typesetting found for |- ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s with typecode |-
162		2sno	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
163		2ne0s	Could not format 2s =/= 0s : No typesetting found for |- 2s =/= 0s with typecode |-
164	162 163	pm3.2i	Could not format ( 2s e. No /\ 2s =/= 0s ) : No typesetting found for |- ( 2s e. No /\ 2s =/= 0s ) with typecode |-
165	8 20 164	3pm3.2i	Could not format ( 1s e. No /\ ( { 0s } |s { 1s } ) e. No /\ ( 2s e. No /\ 2s =/= 0s ) ) : No typesetting found for |- ( 1s e. No /\ ( { 0s } |s { 1s } ) e. No /\ ( 2s e. No /\ 2s =/= 0s ) ) with typecode |-
166		oveq2	Could not format ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) ) : No typesetting found for |- ( x = ( { 0s } |s { 1s } ) -> ( 2s x.s x ) = ( 2s x.s ( { 0s } |s { 1s } ) ) ) with typecode |-
167	166	eqeq1d	Could not format ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) : No typesetting found for |- ( x = ( { 0s } |s { 1s } ) -> ( ( 2s x.s x ) = 1s <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) with typecode |-
168	167	rspcev	Could not format ( ( ( { 0s } |s { 1s } ) e. No /\ ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) -> E. x e. No ( 2s x.s x ) = 1s ) : No typesetting found for |- ( ( ( { 0s } |s { 1s } ) e. No /\ ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) -> E. x e. No ( 2s x.s x ) = 1s ) with typecode |-
169	20 161 168	mp2an	Could not format E. x e. No ( 2s x.s x ) = 1s : No typesetting found for |- E. x e. No ( 2s x.s x ) = 1s with typecode |-
170		divsmulw	Could not format ( ( ( 1s e. No /\ ( { 0s } |s { 1s } ) e. No /\ ( 2s e. No /\ 2s =/= 0s ) ) /\ E. x e. No ( 2s x.s x ) = 1s ) -> ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) : No typesetting found for |- ( ( ( 1s e. No /\ ( { 0s } |s { 1s } ) e. No /\ ( 2s e. No /\ 2s =/= 0s ) ) /\ E. x e. No ( 2s x.s x ) = 1s ) -> ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) ) with typecode |-
171	165 169 170	mp2an	Could not format ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) : No typesetting found for |- ( ( 1s /su 2s ) = ( { 0s } |s { 1s } ) <-> ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s ) with typecode |-
172	161 171	mpbir	Could not format ( 1s /su 2s ) = ( { 0s } |s { 1s } ) : No typesetting found for |- ( 1s /su 2s ) = ( { 0s } |s { 1s } ) with typecode |-