Theorem twocut

Description: Two times the cut of zero and one is one. (Contributed by Scott Fenton, 5-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		0sno	$$⊢0_s\in \mathrm{No}$$
2	1	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
3		1sno	$$⊢1_s\in \mathrm{No}$$
4	3	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
5		0slt1s	$$⊢0_s{<}_s{1}_s$$
6	5	a1i	$$⊢\top \to 0_s{<}_s{1}_s$$
7	2 4 6	ssltsn	$$⊢\top \to \left\{0_s\right\}{\ll }_s\left\{1_s\right\}$$
8	7	scutcld	$$⊢\top \to \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
9	8	mptru	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}$$
10		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 |-
11	9 10	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 |-
12		eqidd	$$⊢\top \to \left\{0_s\right\}{|}_s\left\{1_s\right\}=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
13	7 7 12 12	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)$$
14	13	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)$$
15	1	elexi	$$⊢0_s\in \mathrm{V}$$
16		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)$$
17	16	eqeq2d	$$⊢y=0_s\to \left(x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=0_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
18	15 17	rexsn	$$⊢\exists y\in \left\{0_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=0_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
19		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\}$$
20	9 19	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\}$$
21	20	eqeq2i	$$⊢x=0_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
22	18 21	bitri	$$⊢\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\}$$
23	22	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\}$$
24		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\}$$
25	23 24	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\}$$
26		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$$
27	26	eqeq2d	$$⊢y=0_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{0}_s\right)$$
28	15 27	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(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{0}_s$$
29		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\}$$
30	9 29	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\}$$
31	30	eqeq2i	$$⊢x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{0}_s\leftrightarrow x=\left\{0_s\right\}{|}_s\left\{1_s\right\}$$
32	28 31	bitri	$$⊢\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\}$$
33	32	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\}$$
34	33 24	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\}$$
35	25 34	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\}$$
36		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\}$$
37	35 36	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\}$$
38	3	elexi	$$⊢1_s\in \mathrm{V}$$
39		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)$$
40	39	eqeq2d	$$⊢y=1_s\to \left(x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
41	38 40	rexsn	$$⊢\exists y\in \left\{1_s\right\}x=y{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\leftrightarrow x=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
42	41	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=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
43		df-sn	$$⊢\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{x|x=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
44	42 43	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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
45		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$$
46	45	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)$$
47	38 46	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$$
48		addscom	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
49	9 3 48	mp2an	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
50	49	eqeq2i	$$⊢x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_s{1}_s\leftrightarrow x=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
51	47 50	bitri	$$⊢\exists y\in \left\{1_s\right\}x=\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){+}_{s}y\leftrightarrow x=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
52	51	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=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
53	52 43	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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
54	44 53	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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
55		unidm	$$⊢\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\cup \left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
56	54 55	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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
57	37 56	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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
58		ral0	$$⊢\forall x\in \varnothing \left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right){<}_{s}x$$
59		scutcut	$$⊢\left\{0_s\right\}{\ll }_s\left\{1_s\right\}\to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}\wedge \left\{0_s\right\}{\ll }_s\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\wedge \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{1_s\right\}\right)$$
60	7 59	syl	$$⊢\top \to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{No}\wedge \left\{0_s\right\}{\ll }_s\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}\wedge \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{1_s\right\}\right)$$
61	60	simp3d	$$⊢\top \to \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{1_s\right\}$$
62		ovex	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \mathrm{V}$$
63	62	snid	$$⊢\left\{0_s\right\}{|}_s\left\{1_s\right\}\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
64	63	a1i	$$⊢\top \to \left\{0_s\right\}{|}_s\left\{1_s\right\}\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
65	38	snid	$$⊢1_s\in \left\{1_s\right\}$$
66	65	a1i	$$⊢\top \to 1_s\in \left\{1_s\right\}$$
67	61 64 66	ssltsepcd	$$⊢\top \to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s{1}_s$$
68	67	mptru	$$⊢\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s{1}_s$$
69		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)$$
70	62 69	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$$
71	68 70	mpbir	$$⊢\forall y\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}y{<}_s{1}_s$$
72	4 8	addscld	$$⊢\top \to 1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\in \mathrm{No}$$
73	8	sltp1d	$$⊢\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)$$
74	73 49	breqtrdi	$$⊢\top \to \left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right){<}_s\left(1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
75	8 72 74	ssltsn	$$⊢\top \to \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
76	75	mptru	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
77		snelpwi	$$⊢0_s\in \mathrm{No}\to \left\{0_s\right\}\in 𝒫\mathrm{No}$$
78	1 77	ax-mp	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}$$
79		nulssgt	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}\to \left\{0_s\right\}{\ll }_s\varnothing$$
80	78 79	ax-mp	$$⊢\left\{0_s\right\}{\ll }_s\varnothing$$
81		eqid	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}$$
82		df-1s	$$⊢1_s=\left\{0_s\right\}{|}_s\varnothing$$
83		slerec	$$⊢\left(\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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)$$
84	76 80 81 82 83	mp4an	$$⊢\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right){<}_{s}x\wedge \forall y\in \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}y{<}_s{1}_s\right)$$
85	58 71 84	mpbir2an	$$⊢\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right){\le }_s{1}_s$$
86	60	simp2d	$$⊢\top \to \left\{0_s\right\}{\ll }_s\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}$$
87	15	snid	$$⊢0_s\in \left\{0_s\right\}$$
88	87	a1i	$$⊢\top \to 0_s\in \left\{0_s\right\}$$
89	86 88 64	ssltsepcd	$$⊢\top \to 0_s{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
90	89	mptru	$$⊢0_s{<}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)$$
91		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)$$
92	1 9 3 91	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)$$
93	90 92	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)$$
94		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
95	3 94	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
96	93 95 49	3brtr3i	$$⊢1_s{<}_s\left(1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
97		ovex	$$⊢1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\in \mathrm{V}$$
98		breq2	$$⊢x=1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\to \left(1_s{<}_{s}x\leftrightarrow 1_s{<}_s\left(1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)\right)$$
99	97 98	ralsn	$$⊢\forall x\in \left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}{1}_s{<}_{s}x\leftrightarrow 1_s{<}_s\left(1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right)$$
100	96 99	mpbir	$$⊢\forall x\in \left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}{1}_s{<}_{s}x$$
101	75	scutcld	$$⊢\top \to \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\in \mathrm{No}$$
102		scutcut	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{\ll }_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\to \left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\in \mathrm{No}\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\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right\}\wedge \left\{\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right\}{\ll }_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)$$
103	75 102	syl	$$⊢\top \to \left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\in \mathrm{No}\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\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right\}\wedge \left\{\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right\}{\ll }_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)$$
104	103	simp2d	$$⊢\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\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right\}$$
105		ovex	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\in \mathrm{V}$$
106	105	snid	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\in \left\{\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right\}$$
107	106	a1i	$$⊢\top \to \left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\in \left\{\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right\}$$
108	104 64 107	ssltsepcd	$$⊢\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\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)$$
109	2 8 101 89 108	slttrd	$$⊢\top \to 0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)$$
110	109	mptru	$$⊢0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)$$
111		breq1	$$⊢y=0_s\to \left(y{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\leftrightarrow 0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\right)$$
112	15 111	ralsn	$$⊢\forall y\in \left\{0_s\right\}y{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\leftrightarrow 0_s{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)$$
113	110 112	mpbir	$$⊢\forall y\in \left\{0_s\right\}y{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)$$
114		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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\right)\to \left(1_s{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\leftrightarrow \left(\forall x\in \left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}{1}_s{<}_{s}x\wedge \forall y\in \left\{0_s\right\}y{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\right)\right)$$
115	80 76 82 81 114	mp4an	$$⊢1_s{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\leftrightarrow \left(\forall x\in \left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}{1}_s{<}_{s}x\wedge \forall y\in \left\{0_s\right\}y{<}_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\right)$$
116	100 113 115	mpbir2an	$$⊢1_s{\le }_s\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)$$
117	101	mptru	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\in \mathrm{No}$$
118		sletri3	$$⊢\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=1_s\leftrightarrow \left(\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\right)\right)$$
119	117 3 118	mp2an	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=1_s\leftrightarrow \left(\left(\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\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\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}\right)\right)$$
120	85 116 119	mpbir2an	$$⊢\left\{\left\{0_s\right\}{|}_s\left\{1_s\right\}\right\}{|}_s\left\{1_s{+}_s\left(\left\{0_s\right\}{|}_s\left\{1_s\right\}\right)\right\}=1_s$$
121	57 120	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$$
122	14 121	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$$
123	11 122	eqtri	Could not format ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s : No typesetting found for |- ( 2s x.s ( { 0s } |s { 1s } ) ) = 1s with typecode |-