Theorem twocut 28437

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 27823	. . . . . . 7 ⊢ 0s ∈ No
2	1	a1i 11	. . . . . 6 ⊢ (⊤ → 0s ∈ No )
3		1no 27824	. . . . . . 7 ⊢ 1s ∈ No
4	3	a1i 11	. . . . . 6 ⊢ (⊤ → 1s ∈ No )
5		0lt1s 27826	. . . . . . 7 ⊢ 0s <s 1s
6	5	a1i 11	. . . . . 6 ⊢ (⊤ → 0s <s 1s )
7	2, 4, 6	sltssn 27784	. . . . 5 ⊢ (⊤ → { 0s } <<s { 1s })
8	7	cutscld 27797	. . . 4 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ No )
9	8	mptru 1555	. . 3 ⊢ ({ 0s } |s { 1s }) ∈ No
10		no2times 28431	. . 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 2742	. . . . 5 ⊢ (⊤ → ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))
13	7, 7, 12, 12	addsunif 28016	. . . 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 1555	. . 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 3455	. . . . . . . . . . 11 ⊢ 0s ∈ V
16		oveq1 7367	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ( 0s +s ({ 0s } |s { 1s })))
17	16	eqeq2d 2752	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s }))))
18	15, 17	rexsn 4617	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s })))
19		addslid 27982	. . . . . . . . . . . 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 2754	. . . . . . . . . 10 ⊢ (𝑥 = ( 0s +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s }))
22	18, 21	bitri 277	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s }))
23	22	abbii 2808	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
24		df-sn 4559	. . . . . . . 8 ⊢ {({ 0s } |s { 1s })} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
25	23, 24	eqtr4i 2767	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {({ 0s } |s { 1s })}
26		oveq2 7368	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 0s ))
27	26	eqeq2d 2752	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s )))
28	15, 27	rexsn 4617	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s ))
29		addsrid 27978	. . . . . . . . . . . 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 2754	. . . . . . . . . 10 ⊢ (𝑥 = (({ 0s } |s { 1s }) +s 0s ) ↔ 𝑥 = ({ 0s } |s { 1s }))
32	28, 31	bitri 277	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s }))
33	32	abbii 2808	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
34	33, 24	eqtr4i 2767	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {({ 0s } |s { 1s })}
35	25, 34	uneq12i 4099	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })})
36		unidm 4090	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })}) = {({ 0s } |s { 1s })}
37	35, 36	eqtri 2764	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {({ 0s } |s { 1s })}
38	3	elexi 3455	. . . . . . . . . 10 ⊢ 1s ∈ V
39		oveq1 7367	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = ( 1s +s ({ 0s } |s { 1s })))
40	39	eqeq2d 2752	. . . . . . . . . 10 ⊢ (𝑦 = 1s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))))
41	38, 40	rexsn 4617	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
42	41	abbii 2808	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
43		df-sn 4559	. . . . . . . 8 ⊢ {( 1s +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
44	42, 43	eqtr4i 2767	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {( 1s +s ({ 0s } |s { 1s }))}
45		oveq2 7368	. . . . . . . . . . . 12 ⊢ (𝑦 = 1s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 1s ))
46	45	eqeq2d 2752	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
47	38, 46	rexsn 4617	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
48		addscom 27980	. . . . . . . . . . . 12 ⊢ ((({ 0s } |s { 1s }) ∈ No ∧ 1s ∈ No ) → (({ 0s } |s { 1s }) +s 1s ) = ( 1s +s ({ 0s } |s { 1s })))
49	9, 3, 48	mp2an 699	. . . . . . . . . . 11 ⊢ (({ 0s } |s { 1s }) +s 1s ) = ( 1s +s ({ 0s } |s { 1s }))
50	49	eqeq2i 2754	. . . . . . . . . 10 ⊢ (𝑥 = (({ 0s } |s { 1s }) +s 1s ) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
51	47, 50	bitri 277	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
52	51	abbii 2808	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
53	52, 43	eqtr4i 2767	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {( 1s +s ({ 0s } |s { 1s }))}
54	44, 53	uneq12i 4099	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))})
55		unidm 4090	. . . . . 6 ⊢ ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))}) = {( 1s +s ({ 0s } |s { 1s }))}
56	54, 55	eqtri 2764	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {( 1s +s ({ 0s } |s { 1s }))}
57	37, 56	oveq12i 7372	. . . 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 4429	. . . . . 6 ⊢ ∀𝑥 ∈ ∅ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) <s 𝑥
59		cutcuts 27795	. . . . . . . . . . 11 ⊢ ({ 0s } <<s { 1s } → (({ 0s } |s { 1s }) ∈ No ∧ { 0s } <<s {({ 0s } |s { 1s })} ∧ {({ 0s } |s { 1s })} <<s { 1s }))
60	7, 59	syl 17	. . . . . . . . . 10 ⊢ (⊤ → (({ 0s } |s { 1s }) ∈ No ∧ { 0s } <<s {({ 0s } |s { 1s })} ∧ {({ 0s } |s { 1s })} <<s { 1s }))
61	60	simp3d 1151	. . . . . . . . 9 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s { 1s })
62		ovex 7393	. . . . . . . . . . 11 ⊢ ({ 0s } |s { 1s }) ∈ V
63	62	snid 4597	. . . . . . . . . 10 ⊢ ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })}
64	63	a1i 11	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })})
65	38	snid 4597	. . . . . . . . . 10 ⊢ 1s ∈ { 1s }
66	65	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 1s ∈ { 1s })
67	61, 64, 66	sltssepcd 27786	. . . . . . . 8 ⊢ (⊤ → ({ 0s } |s { 1s }) <s 1s )
68	67	mptru 1555	. . . . . . 7 ⊢ ({ 0s } |s { 1s }) <s 1s
69		breq1 5078	. . . . . . . 8 ⊢ (𝑦 = ({ 0s } |s { 1s }) → (𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s ))
70	62, 69	ralsn 4616	. . . . . . 7 ⊢ (∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s )
71	68, 70	mpbir 233	. . . . . 6 ⊢ ∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s
72	4, 8	addscld 27994	. . . . . . . . 9 ⊢ (⊤ → ( 1s +s ({ 0s } |s { 1s })) ∈ No )
73	8	ltsp1d 28029	. . . . . . . . . 10 ⊢ (⊤ → ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s ))
74	73, 49	breqtrdi 5116	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ( 1s +s ({ 0s } |s { 1s })))
75	8, 72, 74	sltssn 27784	. . . . . . . 8 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {( 1s +s ({ 0s } |s { 1s }))})
76	75	mptru 1555	. . . . . . 7 ⊢ {({ 0s } |s { 1s })} <<s {( 1s +s ({ 0s } |s { 1s }))}
77		snelpwi 5386	. . . . . . . . 9 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
78	1, 77	ax-mp 5	. . . . . . . 8 ⊢ { 0s } ∈ 𝒫 No
79		nulsgts 27790	. . . . . . . 8 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
80	78, 79	ax-mp 5	. . . . . . 7 ⊢ { 0s } <<s ∅
81		eqid 2741	. . . . . . 7 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
82		df-1s 27822	. . . . . . 7 ⊢ 1s = ({ 0s } |s ∅)
83		lesrec 27813	. . . . . . 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 700	. . . . . 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 718	. . . . 5 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ≤s 1s
86	60	simp2d 1150	. . . . . . . . . . 11 ⊢ (⊤ → { 0s } <<s {({ 0s } |s { 1s })})
87	15	snid 4597	. . . . . . . . . . . 12 ⊢ 0s ∈ { 0s }
88	87	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 0s ∈ { 0s })
89	86, 88, 64	sltssepcd 27786	. . . . . . . . . 10 ⊢ (⊤ → 0s <s ({ 0s } |s { 1s }))
90	89	mptru 1555	. . . . . . . . 9 ⊢ 0s <s ({ 0s } |s { 1s })
91		ltadds1 28006	. . . . . . . . . 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 1470	. . . . . . . . 9 ⊢ ( 0s <s ({ 0s } |s { 1s }) ↔ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s ))
93	90, 92	mpbi 232	. . . . . . . 8 ⊢ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s )
94		addslid 27982	. . . . . . . . 9 ⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
95	3, 94	ax-mp 5	. . . . . . . 8 ⊢ ( 0s +s 1s ) = 1s
96	93, 95, 49	3brtr3i 5104	. . . . . . 7 ⊢ 1s <s ( 1s +s ({ 0s } |s { 1s }))
97		ovex 7393	. . . . . . . 8 ⊢ ( 1s +s ({ 0s } |s { 1s })) ∈ V
98		breq2 5079	. . . . . . . 8 ⊢ (𝑥 = ( 1s +s ({ 0s } |s { 1s })) → ( 1s <s 𝑥 ↔ 1s <s ( 1s +s ({ 0s } |s { 1s }))))
99	97, 98	ralsn 4616	. . . . . . 7 ⊢ (∀𝑥 ∈ {( 1s +s ({ 0s } |s { 1s }))} 1s <s 𝑥 ↔ 1s <s ( 1s +s ({ 0s } |s { 1s })))
100	96, 99	mpbir 233	. . . . . 6 ⊢ ∀𝑥 ∈ {( 1s +s ({ 0s } |s { 1s }))} 1s <s 𝑥
101	75	cutscld 27797	. . . . . . . . 9 ⊢ (⊤ → ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No )
102		cutcuts 27795	. . . . . . . . . . . 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 17	. . . . . . . . . . 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 1150	. . . . . . . . . 10 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})})
105		ovex 7393	. . . . . . . . . . . 12 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ V
106	105	snid 4597	. . . . . . . . . . 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 27786	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
109	2, 8, 101, 89, 108	ltstrd 27749	. . . . . . . 8 ⊢ (⊤ → 0s <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
110	109	mptru 1555	. . . . . . 7 ⊢ 0s <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
111		breq1 5078	. . . . . . . 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 4616	. . . . . . 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 233	. . . . . 6 ⊢ ∀𝑦 ∈ { 0s }𝑦 <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
114		lesrec 27813	. . . . . . 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 700	. . . . . 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 718	. . . . 5 ⊢ 1s ≤s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
117	101	mptru 1555	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No
118		lestri3 27741	. . . . . 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 699	. . . . 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 718	. . . 4 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = 1s
121	57, 120	eqtri 2764	. . 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 2764	. 2 ⊢ (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })) = 1s
123	11, 122	eqtri 2764	1 ⊢ (2s ·s ({ 0s } |s { 1s })) = 1s

Syntax hints:   ↔ wb 208   ∧ wa 397   ∧ w3a 1093   = wceq 1548  ⊤wtru 1549   ∈ wcel 2121  {cab 2719  ∀wral 3055  ∃wrex 3065   ∪ cun 3883  ∅c0 4264  𝒫 cpw 4532  {csn 4558   class class class wbr 5075  (class class class)co 7360   No csur 27625   <s clts 27626   ≤s cles 27730   <<s cslts 27771   |s ccuts 27773   0_s c0s 27819   1_s c1s 27820   +_s cadds 27973   ·_s cmuls 28120  2_sc2s 28424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-ot 4567  df-uni 4842  df-int 4881  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-nadd 8596  df-no 27628  df-lts 27629  df-bday 27630  df-les 27731  df-slts 27772  df-cuts 27774  df-0s 27821  df-1s 27822  df-made 27841  df-old 27842  df-left 27844  df-right 27845  df-norec 27952  df-norec2 27963  df-adds 27974  df-negs 28035  df-subs 28036  df-muls 28121  df-n0s 28328  df-2s 28425

This theorem is referenced by:  nohalf  28438  pw2recs  28452  halfcut  28472