Theorem twocut

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

	Ref	Expression
Assertion	twocut	⊢ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s

Proof

Step	Hyp	Ref	Expression
1		0no	⊢ 0s ∈ No
2	1	a1i	⊢ ( ⊤ → 0s ∈ No )
3		1no	⊢ 1s ∈ No
4	3	a1i	⊢ ( ⊤ → 1s ∈ No )
5		0lt1s	⊢ 0s <s 1s
6	5	a1i	⊢ ( ⊤ → 0s <s 1s )
7	2 4 6	sltssn	⊢ ( ⊤ → { 0s } <<s { 1s } )
8	7	cutscld	⊢ ( ⊤ → ( { 0s } |s { 1s } ) ∈ No )
9	8	mptru	⊢ ( { 0s } |s { 1s } ) ∈ No
10		no2times	⊢ ( ( { 0s } |s { 1s } ) ∈ No → ( 2s ·s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) )
11	9 10	ax-mp	⊢ ( 2s ·s ( { 0s } |s { 1s } ) ) = ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) )
12		eqidd	⊢ ( ⊤ → ( { 0s } |s { 1s } ) = ( { 0s } |s { 1s } ) )
13	7 7 12 12	addsunif	⊢ ( ⊤ → ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) ) )
14	13	mptru	⊢ ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) )
15	1	elexi	⊢ 0s ∈ V
16		oveq1	⊢ ( 𝑦 = 0s → ( 𝑦 +s ( { 0s } |s { 1s } ) ) = ( 0s +s ( { 0s } |s { 1s } ) ) )
17	16	eqeq2d	⊢ ( 𝑦 = 0s → ( 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) ↔ 𝑥 = ( 0s +s ( { 0s } |s { 1s } ) ) ) )
18	15 17	rexsn	⊢ ( ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) ↔ 𝑥 = ( 0s +s ( { 0s } |s { 1s } ) ) )
19		addslid	⊢ ( ( { 0s } |s { 1s } ) ∈ No → ( 0s +s ( { 0s } |s { 1s } ) ) = ( { 0s } |s { 1s } ) )
20	9 19	ax-mp	⊢ ( 0s +s ( { 0s } |s { 1s } ) ) = ( { 0s } |s { 1s } )
21	20	eqeq2i	⊢ ( 𝑥 = ( 0s +s ( { 0s } |s { 1s } ) ) ↔ 𝑥 = ( { 0s } |s { 1s } ) )
22	18 21	bitri	⊢ ( ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) ↔ 𝑥 = ( { 0s } |s { 1s } ) )
23	22	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } = { 𝑥 ∣ 𝑥 = ( { 0s } |s { 1s } ) }
24		df-sn	⊢ { ( { 0s } |s { 1s } ) } = { 𝑥 ∣ 𝑥 = ( { 0s } |s { 1s } ) }
25	23 24	eqtr4i	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } = { ( { 0s } |s { 1s } ) }
26		oveq2	⊢ ( 𝑦 = 0s → ( ( { 0s } |s { 1s } ) +s 𝑦 ) = ( ( { 0s } |s { 1s } ) +s 0s ) )
27	26	eqeq2d	⊢ ( 𝑦 = 0s → ( 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) ↔ 𝑥 = ( ( { 0s } |s { 1s } ) +s 0s ) ) )
28	15 27	rexsn	⊢ ( ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) ↔ 𝑥 = ( ( { 0s } |s { 1s } ) +s 0s ) )
29		addsrid	⊢ ( ( { 0s } |s { 1s } ) ∈ No → ( ( { 0s } |s { 1s } ) +s 0s ) = ( { 0s } |s { 1s } ) )
30	9 29	ax-mp	⊢ ( ( { 0s } |s { 1s } ) +s 0s ) = ( { 0s } |s { 1s } )
31	30	eqeq2i	⊢ ( 𝑥 = ( ( { 0s } |s { 1s } ) +s 0s ) ↔ 𝑥 = ( { 0s } |s { 1s } ) )
32	28 31	bitri	⊢ ( ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) ↔ 𝑥 = ( { 0s } |s { 1s } ) )
33	32	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } = { 𝑥 ∣ 𝑥 = ( { 0s } |s { 1s } ) }
34	33 24	eqtr4i	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } = { ( { 0s } |s { 1s } ) }
35	25 34	uneq12i	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) = ( { ( { 0s } |s { 1s } ) } ∪ { ( { 0s } |s { 1s } ) } )
36		unidm	⊢ ( { ( { 0s } |s { 1s } ) } ∪ { ( { 0s } |s { 1s } ) } ) = { ( { 0s } |s { 1s } ) }
37	35 36	eqtri	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) = { ( { 0s } |s { 1s } ) }
38	3	elexi	⊢ 1s ∈ V
39		oveq1	⊢ ( 𝑦 = 1s → ( 𝑦 +s ( { 0s } |s { 1s } ) ) = ( 1s +s ( { 0s } |s { 1s } ) ) )
40	39	eqeq2d	⊢ ( 𝑦 = 1s → ( 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) ↔ 𝑥 = ( 1s +s ( { 0s } |s { 1s } ) ) ) )
41	38 40	rexsn	⊢ ( ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) ↔ 𝑥 = ( 1s +s ( { 0s } |s { 1s } ) ) )
42	41	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } = { 𝑥 ∣ 𝑥 = ( 1s +s ( { 0s } |s { 1s } ) ) }
43		df-sn	⊢ { ( 1s +s ( { 0s } |s { 1s } ) ) } = { 𝑥 ∣ 𝑥 = ( 1s +s ( { 0s } |s { 1s } ) ) }
44	42 43	eqtr4i	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } = { ( 1s +s ( { 0s } |s { 1s } ) ) }
45		oveq2	⊢ ( 𝑦 = 1s → ( ( { 0s } |s { 1s } ) +s 𝑦 ) = ( ( { 0s } |s { 1s } ) +s 1s ) )
46	45	eqeq2d	⊢ ( 𝑦 = 1s → ( 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) ↔ 𝑥 = ( ( { 0s } |s { 1s } ) +s 1s ) ) )
47	38 46	rexsn	⊢ ( ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) ↔ 𝑥 = ( ( { 0s } |s { 1s } ) +s 1s ) )
48		addscom	⊢ ( ( ( { 0s } |s { 1s } ) ∈ No ∧ 1s ∈ No ) → ( ( { 0s } |s { 1s } ) +s 1s ) = ( 1s +s ( { 0s } |s { 1s } ) ) )
49	9 3 48	mp2an	⊢ ( ( { 0s } |s { 1s } ) +s 1s ) = ( 1s +s ( { 0s } |s { 1s } ) )
50	49	eqeq2i	⊢ ( 𝑥 = ( ( { 0s } |s { 1s } ) +s 1s ) ↔ 𝑥 = ( 1s +s ( { 0s } |s { 1s } ) ) )
51	47 50	bitri	⊢ ( ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) ↔ 𝑥 = ( 1s +s ( { 0s } |s { 1s } ) ) )
52	51	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } = { 𝑥 ∣ 𝑥 = ( 1s +s ( { 0s } |s { 1s } ) ) }
53	52 43	eqtr4i	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } = { ( 1s +s ( { 0s } |s { 1s } ) ) }
54	44 53	uneq12i	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) = ( { ( 1s +s ( { 0s } |s { 1s } ) ) } ∪ { ( 1s +s ( { 0s } |s { 1s } ) ) } )
55		unidm	⊢ ( { ( 1s +s ( { 0s } |s { 1s } ) ) } ∪ { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = { ( 1s +s ( { 0s } |s { 1s } ) ) }
56	54 55	eqtri	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) = { ( 1s +s ( { 0s } |s { 1s } ) ) }
57	37 56	oveq12i	⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) ) = ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
58		ral0	⊢ ∀ 𝑥 ∈ ∅ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <s 𝑥
59		cutcuts	⊢ ( { 0s } <<s { 1s } → ( ( { 0s } |s { 1s } ) ∈ No ∧ { 0s } <<s { ( { 0s } |s { 1s } ) } ∧ { ( { 0s } |s { 1s } ) } <<s { 1s } ) )
60	7 59	syl	⊢ ( ⊤ → ( ( { 0s } |s { 1s } ) ∈ No ∧ { 0s } <<s { ( { 0s } |s { 1s } ) } ∧ { ( { 0s } |s { 1s } ) } <<s { 1s } ) )
61	60	simp3d	⊢ ( ⊤ → { ( { 0s } |s { 1s } ) } <<s { 1s } )
62		ovex	⊢ ( { 0s } |s { 1s } ) ∈ V
63	62	snid	⊢ ( { 0s } |s { 1s } ) ∈ { ( { 0s } |s { 1s } ) }
64	63	a1i	⊢ ( ⊤ → ( { 0s } |s { 1s } ) ∈ { ( { 0s } |s { 1s } ) } )
65	38	snid	⊢ 1s ∈ { 1s }
66	65	a1i	⊢ ( ⊤ → 1s ∈ { 1s } )
67	61 64 66	sltssepcd	⊢ ( ⊤ → ( { 0s } |s { 1s } ) <s 1s )
68	67	mptru	⊢ ( { 0s } |s { 1s } ) <s 1s
69		breq1	⊢ ( 𝑦 = ( { 0s } |s { 1s } ) → ( 𝑦 <s 1s ↔ ( { 0s } |s { 1s } ) <s 1s ) )
70	62 69	ralsn	⊢ ( ∀ 𝑦 ∈ { ( { 0s } |s { 1s } ) } 𝑦 <s 1s ↔ ( { 0s } |s { 1s } ) <s 1s )
71	68 70	mpbir	⊢ ∀ 𝑦 ∈ { ( { 0s } |s { 1s } ) } 𝑦 <s 1s
72	4 8	addscld	⊢ ( ⊤ → ( 1s +s ( { 0s } |s { 1s } ) ) ∈ No )
73	8	ltsp1d	⊢ ( ⊤ → ( { 0s } |s { 1s } ) <s ( ( { 0s } |s { 1s } ) +s 1s ) )
74	73 49	breqtrdi	⊢ ( ⊤ → ( { 0s } |s { 1s } ) <s ( 1s +s ( { 0s } |s { 1s } ) ) )
75	8 72 74	sltssn	⊢ ( ⊤ → { ( { 0s } |s { 1s } ) } <<s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
76	75	mptru	⊢ { ( { 0s } |s { 1s } ) } <<s { ( 1s +s ( { 0s } |s { 1s } ) ) }
77		snelpwi	⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
78	1 77	ax-mp	⊢ { 0s } ∈ 𝒫 No
79		nulsgts	⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
80	78 79	ax-mp	⊢ { 0s } <<s ∅
81		eqid	⊢ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
82		df-1s	⊢ 1s = ( { 0s } |s ∅ )
83		lesrec	⊢ ( ( ( { ( { 0s } |s { 1s } ) } <<s { ( 1s +s ( { 0s } |s { 1s } ) ) } ∧ { 0s } <<s ∅ ) ∧ ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∧ 1s = ( { 0s } |s ∅ ) ) ) → ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ≤s 1s ↔ ( ∀ 𝑥 ∈ ∅ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <s 𝑥 ∧ ∀ 𝑦 ∈ { ( { 0s } |s { 1s } ) } 𝑦 <s 1s ) ) )
84	76 80 81 82 83	mp4an	⊢ ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ≤s 1s ↔ ( ∀ 𝑥 ∈ ∅ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) <s 𝑥 ∧ ∀ 𝑦 ∈ { ( { 0s } |s { 1s } ) } 𝑦 <s 1s ) )
85	58 71 84	mpbir2an	⊢ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ≤s 1s
86	60	simp2d	⊢ ( ⊤ → { 0s } <<s { ( { 0s } |s { 1s } ) } )
87	15	snid	⊢ 0s ∈ { 0s }
88	87	a1i	⊢ ( ⊤ → 0s ∈ { 0s } )
89	86 88 64	sltssepcd	⊢ ( ⊤ → 0s <s ( { 0s } |s { 1s } ) )
90	89	mptru	⊢ 0s <s ( { 0s } |s { 1s } )
91		ltadds1	⊢ ( ( 0s ∈ No ∧ ( { 0s } |s { 1s } ) ∈ No ∧ 1s ∈ No ) → ( 0s <s ( { 0s } |s { 1s } ) ↔ ( 0s +s 1s ) <s ( ( { 0s } |s { 1s } ) +s 1s ) ) )
92	1 9 3 91	mp3an	⊢ ( 0s <s ( { 0s } |s { 1s } ) ↔ ( 0s +s 1s ) <s ( ( { 0s } |s { 1s } ) +s 1s ) )
93	90 92	mpbi	⊢ ( 0s +s 1s ) <s ( ( { 0s } |s { 1s } ) +s 1s )
94		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
95	3 94	ax-mp	⊢ ( 0s +s 1s ) = 1s
96	93 95 49	3brtr3i	⊢ 1s <s ( 1s +s ( { 0s } |s { 1s } ) )
97		ovex	⊢ ( 1s +s ( { 0s } |s { 1s } ) ) ∈ V
98		breq2	⊢ ( 𝑥 = ( 1s +s ( { 0s } |s { 1s } ) ) → ( 1s <s 𝑥 ↔ 1s <s ( 1s +s ( { 0s } |s { 1s } ) ) ) )
99	97 98	ralsn	⊢ ( ∀ 𝑥 ∈ { ( 1s +s ( { 0s } |s { 1s } ) ) } 1s <s 𝑥 ↔ 1s <s ( 1s +s ( { 0s } |s { 1s } ) ) )
100	96 99	mpbir	⊢ ∀ 𝑥 ∈ { ( 1s +s ( { 0s } |s { 1s } ) ) } 1s <s 𝑥
101	75	cutscld	⊢ ( ⊤ → ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∈ No )
102		cutcuts	⊢ ( { ( { 0s } |s { 1s } ) } <<s { ( 1s +s ( { 0s } |s { 1s } ) ) } → ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∈ No ∧ { ( { 0s } |s { 1s } ) } <<s { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) } ∧ { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) } <<s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) )
103	75 102	syl	⊢ ( ⊤ → ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∈ No ∧ { ( { 0s } |s { 1s } ) } <<s { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) } ∧ { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) } <<s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) )
104	103	simp2d	⊢ ( ⊤ → { ( { 0s } |s { 1s } ) } <<s { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) } )
105		ovex	⊢ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∈ V
106	105	snid	⊢ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∈ { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) }
107	106	a1i	⊢ ( ⊤ → ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∈ { ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) } )
108	104 64 107	sltssepcd	⊢ ( ⊤ → ( { 0s } |s { 1s } ) <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) )
109	2 8 101 89 108	ltstrd	⊢ ( ⊤ → 0s <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) )
110	109	mptru	⊢ 0s <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
111		breq1	⊢ ( 𝑦 = 0s → ( 𝑦 <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ↔ 0s <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ) )
112	15 111	ralsn	⊢ ( ∀ 𝑦 ∈ { 0s } 𝑦 <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ↔ 0s <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) )
113	110 112	mpbir	⊢ ∀ 𝑦 ∈ { 0s } 𝑦 <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
114		lesrec	⊢ ( ( ( { 0s } <<s ∅ ∧ { ( { 0s } |s { 1s } ) } <<s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∧ ( 1s = ( { 0s } |s ∅ ) ∧ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ) ) → ( 1s ≤s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ↔ ( ∀ 𝑥 ∈ { ( 1s +s ( { 0s } |s { 1s } ) ) } 1s <s 𝑥 ∧ ∀ 𝑦 ∈ { 0s } 𝑦 <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ) ) )
115	80 76 82 81 114	mp4an	⊢ ( 1s ≤s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ↔ ( ∀ 𝑥 ∈ { ( 1s +s ( { 0s } |s { 1s } ) ) } 1s <s 𝑥 ∧ ∀ 𝑦 ∈ { 0s } 𝑦 <s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ) )
116	100 113 115	mpbir2an	⊢ 1s ≤s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } )
117	101	mptru	⊢ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∈ No
118		lestri3	⊢ ( ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ∈ No ∧ 1s ∈ No ) → ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = 1s ↔ ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ≤s 1s ∧ 1s ≤s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ) ) )
119	117 3 118	mp2an	⊢ ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = 1s ↔ ( ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ≤s 1s ∧ 1s ≤s ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) ) )
120	85 116 119	mpbir2an	⊢ ( { ( { 0s } |s { 1s } ) } |s { ( 1s +s ( { 0s } |s { 1s } ) ) } ) = 1s
121	57 120	eqtri	⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( 𝑦 +s ( { 0s } |s { 1s } ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 1s } 𝑥 = ( ( { 0s } |s { 1s } ) +s 𝑦 ) } ) ) = 1s
122	14 121	eqtri	⊢ ( ( { 0s } |s { 1s } ) +s ( { 0s } |s { 1s } ) ) = 1s
123	11 122	eqtri	⊢ ( 2s ·s ( { 0s } |s { 1s } ) ) = 1s