Theorem twocut 28836

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

Assertion

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

Proof of Theorem twocut

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0no 28222	. . . . . . 7 ⊢ 0s ∈ No
2	1	a1i 11	. . . . . 6 ⊢ (⊤ → 0s ∈ No)
3		1no 28223	. . . . . . 7 ⊢ 1s ∈ No
4	3	a1i 11	. . . . . 6 ⊢ (⊤ → 1s ∈ No)
5		0lt1s 28225	. . . . . . 7 ⊢ 0s <s 1s
6	5	a1i 11	. . . . . 6 ⊢ (⊤ → 0s <s 1s )
7	2, 4, 6	sltssn 28183	. . . . 5 ⊢ (⊤ → { 0s } <<s { 1s })
8	7	cutscld 28196	. . . 4 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ No)
9	8	mptru 1577	. . 3 ⊢ ({ 0s } |s { 1s }) ∈ No
10		no2times 28830	. . 3 ⊢ (({ 0s } |s { 1s }) ∈ No → (2s ·s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })))
11	9, 10	ax-mp 5	. 2 ⊢ (2s ·s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s }))
12		eqidd 2764	. . . . 5 ⊢ (⊤ → ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))
13	7, 7, 12, 12	addsunif 28415	. . . 4 ⊢ (⊤ → (({ 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 1577	. . 3 ⊢ (({ 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 3476	. . . . . . . . . . 11 ⊢ 0s ∈ V
16		oveq1 7447	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ( 0s +s ({ 0s } |s { 1s })))
17	16	eqeq2d 2774	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s }))))
18	15, 17	rexsn 4643	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s })))
19		addslid 28381	. . . . . . . . . . . 12 ⊢ (({ 0s } |s { 1s }) ∈ No → ( 0s +s ({ 0s } |s { 1s })) = ({ 0s } |s { 1s }))
20	9, 19	ax-mp 5	. . . . . . . . . . 11 ⊢ ( 0s +s ({ 0s } |s { 1s })) = ({ 0s } |s { 1s })
21	20	eqeq2i 2776	. . . . . . . . . 10 ⊢ (𝑥 = ( 0s +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s }))
22	18, 21	bitri 278	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s }))
23	22	abbii 2830	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
24		df-sn 4589	. . . . . . . 8 ⊢ {({ 0s } |s { 1s })} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
25	23, 24	eqtr4i 2789	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {({ 0s } |s { 1s })}
26		oveq2 7448	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 0s ))
27	26	eqeq2d 2774	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s )))
28	15, 27	rexsn 4643	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s ))
29		addsrid 28377	. . . . . . . . . . . 12 ⊢ (({ 0s } |s { 1s }) ∈ No → (({ 0s } |s { 1s }) +s 0s ) = ({ 0s } |s { 1s }))
30	9, 29	ax-mp 5	. . . . . . . . . . 11 ⊢ (({ 0s } |s { 1s }) +s 0s ) = ({ 0s } |s { 1s })
31	30	eqeq2i 2776	. . . . . . . . . 10 ⊢ (𝑥 = (({ 0s } |s { 1s }) +s 0s ) ↔ 𝑥 = ({ 0s } |s { 1s }))
32	28, 31	bitri 278	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s }))
33	32	abbii 2830	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
34	33, 24	eqtr4i 2789	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {({ 0s } |s { 1s })}
35	25, 34	uneq12i 4168	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })})
36		unidm 4159	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })}) = {({ 0s } |s { 1s })}
37	35, 36	eqtri 2786	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {({ 0s } |s { 1s })}
38	3	elexi 3476	. . . . . . . . . 10 ⊢ 1s ∈ V
39		oveq1 7447	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = ( 1s +s ({ 0s } |s { 1s })))
40	39	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑦 = 1s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))))
41	38, 40	rexsn 4643	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
42	41	abbii 2830	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
43		df-sn 4589	. . . . . . . 8 ⊢ {( 1s +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
44	42, 43	eqtr4i 2789	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {( 1s +s ({ 0s } |s { 1s }))}
45		oveq2 7448	. . . . . . . . . . . 12 ⊢ (𝑦 = 1s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 1s ))
46	45	eqeq2d 2774	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
47	38, 46	rexsn 4643	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
48		addscom 28379	. . . . . . . . . . . 12 ⊢ ((({ 0s } |s { 1s }) ∈ No ∧ 1s ∈ No) → (({ 0s } |s { 1s }) +s 1s ) = ( 1s +s ({ 0s } |s { 1s })))
49	9, 3, 48	mp2an 705	. . . . . . . . . . 11 ⊢ (({ 0s } |s { 1s }) +s 1s ) = ( 1s +s ({ 0s } |s { 1s }))
50	49	eqeq2i 2776	. . . . . . . . . 10 ⊢ (𝑥 = (({ 0s } |s { 1s }) +s 1s ) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
51	47, 50	bitri 278	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
52	51	abbii 2830	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
53	52, 43	eqtr4i 2789	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {( 1s +s ({ 0s } |s { 1s }))}
54	44, 53	uneq12i 4168	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))})
55		unidm 4159	. . . . . 6 ⊢ ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))}) = {( 1s +s ({ 0s } |s { 1s }))}
56	54, 55	eqtri 2786	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {( 1s +s ({ 0s } |s { 1s }))}
57	37, 56	oveq12i 7452	. . . 4 ⊢ (({𝑥 ∣ ∃𝑦 ∈ { 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 4457	. . . . . 6 ⊢ ∀𝑥 ∈ ∅ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) <s 𝑥
59		cutcuts 28194	. . . . . . . . . . 11 ⊢ ({ 0s } <<s { 1s } → (({ 0s } |s { 1s }) ∈ No ∧ { 0s } <<s {({ 0s } |s { 1s })} ∧ {({ 0s } |s { 1s })} <<s { 1s }))
60	7, 59	syl 18	. . . . . . . . . 10 ⊢ (⊤ → (({ 0s } |s { 1s }) ∈ No ∧ { 0s } <<s {({ 0s } |s { 1s })} ∧ {({ 0s } |s { 1s })} <<s { 1s }))
61	60	simp3d 1162	. . . . . . . . 9 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s { 1s })
62		ovex 7473	. . . . . . . . . . 11 ⊢ ({ 0s } |s { 1s }) ∈ V
63	62	snid 4623	. . . . . . . . . 10 ⊢ ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })}
64	63	a1i 11	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })})
65	38	snid 4623	. . . . . . . . . 10 ⊢ 1s ∈ { 1s }
66	65	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 1s ∈ { 1s })
67	61, 64, 66	sltssepcd 28185	. . . . . . . 8 ⊢ (⊤ → ({ 0s } |s { 1s }) <s 1s )
68	67	mptru 1577	. . . . . . 7 ⊢ ({ 0s } |s { 1s }) <s 1s
69		breq1 5109	. . . . . . . 8 ⊢ (𝑦 = ({ 0s } |s { 1s }) → (𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s ))
70	62, 69	ralsn 4642	. . . . . . 7 ⊢ (∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s )
71	68, 70	mpbir 234	. . . . . 6 ⊢ ∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s
72	4, 8	addscld 28393	. . . . . . . . 9 ⊢ (⊤ → ( 1s +s ({ 0s } |s { 1s })) ∈ No)
73	8	ltsp1d 28428	. . . . . . . . . 10 ⊢ (⊤ → ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s ))
74	73, 49	breqtrdi 5149	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ( 1s +s ({ 0s } |s { 1s })))
75	8, 72, 74	sltssn 28183	. . . . . . . 8 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {( 1s +s ({ 0s } |s { 1s }))})
76	75	mptru 1577	. . . . . . 7 ⊢ {({ 0s } |s { 1s })} <<s {( 1s +s ({ 0s } |s { 1s }))}
77		snelpwi 5416	. . . . . . . . 9 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No)
78	1, 77	ax-mp 5	. . . . . . . 8 ⊢ { 0s } ∈ 𝒫 No
79		nulsgts 28189	. . . . . . . 8 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
80	78, 79	ax-mp 5	. . . . . . 7 ⊢ { 0s } <<s ∅
81		eqid 2763	. . . . . . 7 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
82		df-1s 28221	. . . . . . 7 ⊢ 1s = ({ 0s } |s ∅)
83		lesrec 28212	. . . . . . 7 ⊢ ((({({ 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 706	. . . . . 6 ⊢ (({({ 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 724	. . . . 5 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ≤s 1s
86	60	simp2d 1161	. . . . . . . . . . 11 ⊢ (⊤ → { 0s } <<s {({ 0s } |s { 1s })})
87	15	snid 4623	. . . . . . . . . . . 12 ⊢ 0s ∈ { 0s }
88	87	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 0s ∈ { 0s })
89	86, 88, 64	sltssepcd 28185	. . . . . . . . . 10 ⊢ (⊤ → 0s <s ({ 0s } |s { 1s }))
90	89	mptru 1577	. . . . . . . . 9 ⊢ 0s <s ({ 0s } |s { 1s })
91		ltadds1 28405	. . . . . . . . . 10 ⊢ (( 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 1491	. . . . . . . . 9 ⊢ ( 0s <s ({ 0s } |s { 1s }) ↔ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s ))
93	90, 92	mpbi 233	. . . . . . . 8 ⊢ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s )
94		addslid 28381	. . . . . . . . 9 ⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
95	3, 94	ax-mp 5	. . . . . . . 8 ⊢ ( 0s +s 1s ) = 1s
96	93, 95, 49	3brtr3i 5137	. . . . . . 7 ⊢ 1s <s ( 1s +s ({ 0s } |s { 1s }))
97		ovex 7473	. . . . . . . 8 ⊢ ( 1s +s ({ 0s } |s { 1s })) ∈ V
98		breq2 5110	. . . . . . . 8 ⊢ (𝑥 = ( 1s +s ({ 0s } |s { 1s })) → ( 1s <s 𝑥 ↔ 1s <s ( 1s +s ({ 0s } |s { 1s }))))
99	97, 98	ralsn 4642	. . . . . . 7 ⊢ (∀𝑥 ∈ {( 1s +s ({ 0s } |s { 1s }))} 1s <s 𝑥 ↔ 1s <s ( 1s +s ({ 0s } |s { 1s })))
100	96, 99	mpbir 234	. . . . . 6 ⊢ ∀𝑥 ∈ {( 1s +s ({ 0s } |s { 1s }))} 1s <s 𝑥
101	75	cutscld 28196	. . . . . . . . 9 ⊢ (⊤ → ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No)
102		cutcuts 28194	. . . . . . . . . . . 12 ⊢ ({({ 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 18	. . . . . . . . . . 11 ⊢ (⊤ → (({({ 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 1161	. . . . . . . . . 10 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})})
105		ovex 7473	. . . . . . . . . . . 12 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ V
106	105	snid 4623	. . . . . . . . . . 11 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ {({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})}
107	106	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ {({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})})
108	104, 64, 107	sltssepcd 28185	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
109	2, 8, 101, 89, 108	ltstrd 28147	. . . . . . . 8 ⊢ (⊤ → 0s <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
110	109	mptru 1577	. . . . . . 7 ⊢ 0s <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
111		breq1 5109	. . . . . . . 8 ⊢ (𝑦 = 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 4642	. . . . . . 7 ⊢ (∀𝑦 ∈ { 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 234	. . . . . 6 ⊢ ∀𝑦 ∈ { 0s }𝑦 <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
114		lesrec 28212	. . . . . . 7 ⊢ ((({ 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 706	. . . . . 6 ⊢ ( 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 724	. . . . 5 ⊢ 1s ≤s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
117	101	mptru 1577	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No
118		lestri3 28139	. . . . . 6 ⊢ ((({({ 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 705	. . . . 5 ⊢ (({({ 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 724	. . . 4 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = 1s
121	57, 120	eqtri 2786	. . 3 ⊢ (({𝑥 ∣ ∃𝑦 ∈ { 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 2786	. 2 ⊢ (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })) = 1s
123	11, 122	eqtri 2786	1 ⊢ (2s ·s ({ 0s } |s { 1s })) = 1s

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ⊤wtru 1571   ∈ wcel 2147  {cab 2741  ∀wral 3080  ∃wrex 3090   ∪ cun 4152  ∅c0 4281  𝒫 cpw 4560  {csn 4588   class class class wbr 5106  (class class class)co 7440  Nocsur 28024   <s clts 28025   ≤s cles 28128   <<s cslts 28170   |s ccuts 28172   0_s c0s 28218   1_s c1s 28219   +_s cadds 28372   ·_s cmuls 28519  2_sc2s 28823

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-ot 4862  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-1st 8022  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-2o 8502  df-nadd 8700  df-no 28027  df-lts 28028  df-bday 28029  df-les 28129  df-slts 28171  df-cuts 28173  df-0s 28220  df-1s 28221  df-made 28240  df-old 28241  df-left 28243  df-right 28244  df-norec 28351  df-norec2 28362  df-adds 28373  df-negs 28434  df-subs 28435  df-muls 28520  df-n0s 28727  df-2s 28824

This theorem is used by:  nohalf  28837  pw2recs  28851  halfcut  28871