Theorem twocut 28582

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 27968	. . . . . . 7 ⊢ 0s ∈ No
2	1	a1i 11	. . . . . 6 ⊢ (⊤ → 0s ∈ No )
3		1no 27969	. . . . . . 7 ⊢ 1s ∈ No
4	3	a1i 11	. . . . . 6 ⊢ (⊤ → 1s ∈ No )
5		0lt1s 27971	. . . . . . 7 ⊢ 0s <s 1s
6	5	a1i 11	. . . . . 6 ⊢ (⊤ → 0s <s 1s )
7	2, 4, 6	sltssn 27929	. . . . 5 ⊢ (⊤ → { 0s } <<s { 1s })
8	7	cutscld 27942	. . . 4 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ No )
9	8	mptru 1574	. . 3 ⊢ ({ 0s } |s { 1s }) ∈ No
10		no2times 28576	. . 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 2770	. . . . 5 ⊢ (⊤ → ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))
13	7, 7, 12, 12	addsunif 28161	. . . 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 1574	. . 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 3483	. . . . . . . . . . 11 ⊢ 0s ∈ V
16		oveq1 7418	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ( 0s +s ({ 0s } |s { 1s })))
17	16	eqeq2d 2780	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s }))))
18	15, 17	rexsn 4651	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s })))
19		addslid 28127	. . . . . . . . . . . 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 2782	. . . . . . . . . 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 2836	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
24		df-sn 4593	. . . . . . . 8 ⊢ {({ 0s } |s { 1s })} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
25	23, 24	eqtr4i 2795	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {({ 0s } |s { 1s })}
26		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 0s ))
27	26	eqeq2d 2780	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s )))
28	15, 27	rexsn 4651	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s ))
29		addsrid 28123	. . . . . . . . . . . 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 2782	. . . . . . . . . 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 2836	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
34	33, 24	eqtr4i 2795	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {({ 0s } |s { 1s })}
35	25, 34	uneq12i 4126	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })})
36		unidm 4117	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })}) = {({ 0s } |s { 1s })}
37	35, 36	eqtri 2792	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {({ 0s } |s { 1s })}
38	3	elexi 3483	. . . . . . . . . 10 ⊢ 1s ∈ V
39		oveq1 7418	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = ( 1s +s ({ 0s } |s { 1s })))
40	39	eqeq2d 2780	. . . . . . . . . 10 ⊢ (𝑦 = 1s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))))
41	38, 40	rexsn 4651	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
42	41	abbii 2836	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
43		df-sn 4593	. . . . . . . 8 ⊢ {( 1s +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
44	42, 43	eqtr4i 2795	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {( 1s +s ({ 0s } |s { 1s }))}
45		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝑦 = 1s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 1s ))
46	45	eqeq2d 2780	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
47	38, 46	rexsn 4651	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
48		addscom 28125	. . . . . . . . . . . 12 ⊢ ((({ 0s } |s { 1s }) ∈ No ∧ 1s ∈ No ) → (({ 0s } |s { 1s }) +s 1s ) = ( 1s +s ({ 0s } |s { 1s })))
49	9, 3, 48	mp2an 704	. . . . . . . . . . 11 ⊢ (({ 0s } |s { 1s }) +s 1s ) = ( 1s +s ({ 0s } |s { 1s }))
50	49	eqeq2i 2782	. . . . . . . . . 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 2836	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
53	52, 43	eqtr4i 2795	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {( 1s +s ({ 0s } |s { 1s }))}
54	44, 53	uneq12i 4126	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))})
55		unidm 4117	. . . . . 6 ⊢ ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))}) = {( 1s +s ({ 0s } |s { 1s }))}
56	54, 55	eqtri 2792	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {( 1s +s ({ 0s } |s { 1s }))}
57	37, 56	oveq12i 7423	. . . 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 4462	. . . . . 6 ⊢ ∀𝑥 ∈ ∅ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) <s 𝑥
59		cutcuts 27940	. . . . . . . . . . 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 1160	. . . . . . . . 9 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s { 1s })
62		ovex 7444	. . . . . . . . . . 11 ⊢ ({ 0s } |s { 1s }) ∈ V
63	62	snid 4631	. . . . . . . . . 10 ⊢ ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })}
64	63	a1i 11	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })})
65	38	snid 4631	. . . . . . . . . 10 ⊢ 1s ∈ { 1s }
66	65	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 1s ∈ { 1s })
67	61, 64, 66	sltssepcd 27931	. . . . . . . 8 ⊢ (⊤ → ({ 0s } |s { 1s }) <s 1s )
68	67	mptru 1574	. . . . . . 7 ⊢ ({ 0s } |s { 1s }) <s 1s
69		breq1 5114	. . . . . . . 8 ⊢ (𝑦 = ({ 0s } |s { 1s }) → (𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s ))
70	62, 69	ralsn 4650	. . . . . . 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 28139	. . . . . . . . 9 ⊢ (⊤ → ( 1s +s ({ 0s } |s { 1s })) ∈ No )
73	8	ltsp1d 28174	. . . . . . . . . 10 ⊢ (⊤ → ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s ))
74	73, 49	breqtrdi 5154	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ( 1s +s ({ 0s } |s { 1s })))
75	8, 72, 74	sltssn 27929	. . . . . . . 8 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {( 1s +s ({ 0s } |s { 1s }))})
76	75	mptru 1574	. . . . . . 7 ⊢ {({ 0s } |s { 1s })} <<s {( 1s +s ({ 0s } |s { 1s }))}
77		snelpwi 5426	. . . . . . . . 9 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
78	1, 77	ax-mp 5	. . . . . . . 8 ⊢ { 0s } ∈ 𝒫 No
79		nulsgts 27935	. . . . . . . 8 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
80	78, 79	ax-mp 5	. . . . . . 7 ⊢ { 0s } <<s ∅
81		eqid 2769	. . . . . . 7 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
82		df-1s 27967	. . . . . . 7 ⊢ 1s = ({ 0s } |s ∅)
83		lesrec 27958	. . . . . . 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 705	. . . . . 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 723	. . . . 5 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ≤s 1s
86	60	simp2d 1159	. . . . . . . . . . 11 ⊢ (⊤ → { 0s } <<s {({ 0s } |s { 1s })})
87	15	snid 4631	. . . . . . . . . . . 12 ⊢ 0s ∈ { 0s }
88	87	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 0s ∈ { 0s })
89	86, 88, 64	sltssepcd 27931	. . . . . . . . . 10 ⊢ (⊤ → 0s <s ({ 0s } |s { 1s }))
90	89	mptru 1574	. . . . . . . . 9 ⊢ 0s <s ({ 0s } |s { 1s })
91		ltadds1 28151	. . . . . . . . . 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 1487	. . . . . . . . 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 28127	. . . . . . . . 9 ⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
95	3, 94	ax-mp 5	. . . . . . . 8 ⊢ ( 0s +s 1s ) = 1s
96	93, 95, 49	3brtr3i 5142	. . . . . . 7 ⊢ 1s <s ( 1s +s ({ 0s } |s { 1s }))
97		ovex 7444	. . . . . . . 8 ⊢ ( 1s +s ({ 0s } |s { 1s })) ∈ V
98		breq2 5115	. . . . . . . 8 ⊢ (𝑥 = ( 1s +s ({ 0s } |s { 1s })) → ( 1s <s 𝑥 ↔ 1s <s ( 1s +s ({ 0s } |s { 1s }))))
99	97, 98	ralsn 4650	. . . . . . 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 27942	. . . . . . . . 9 ⊢ (⊤ → ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No )
102		cutcuts 27940	. . . . . . . . . . . 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 1159	. . . . . . . . . 10 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})})
105		ovex 7444	. . . . . . . . . . . 12 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ V
106	105	snid 4631	. . . . . . . . . . 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 27931	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
109	2, 8, 101, 89, 108	ltstrd 27893	. . . . . . . 8 ⊢ (⊤ → 0s <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
110	109	mptru 1574	. . . . . . 7 ⊢ 0s <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
111		breq1 5114	. . . . . . . 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 4650	. . . . . . 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 27958	. . . . . . 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 705	. . . . . 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 723	. . . . 5 ⊢ 1s ≤s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
117	101	mptru 1574	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No
118		lestri3 27885	. . . . . 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 704	. . . . 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 723	. . . 4 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = 1s
121	57, 120	eqtri 2792	. . 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 2792	. 2 ⊢ (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })) = 1s
123	11, 122	eqtri 2792	1 ⊢ (2s ·s ({ 0s } |s { 1s })) = 1s

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567  ⊤wtru 1568   ∈ wcel 2149  {cab 2747  ∀wral 3085  ∃wrex 3095   ∪ cun 3909  ∅c0 4292  𝒫 cpw 4565  {csn 4592   class class class wbr 5111  (class class class)co 7411   No csur 27770   <s clts 27771   ≤s cles 27874   <<s cslts 27916   |s ccuts 27918   0_s c0s 27964   1_s c1s 27965   +_s cadds 28118   ·_s cmuls 28265  2_sc2s 28569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3375  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-ot 4601  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-nadd 8652  df-no 27773  df-lts 27774  df-bday 27775  df-les 27875  df-slts 27917  df-cuts 27919  df-0s 27966  df-1s 27967  df-made 27986  df-old 27987  df-left 27989  df-right 27990  df-norec 28097  df-norec2 28108  df-adds 28119  df-negs 28180  df-subs 28181  df-muls 28266  df-n0s 28473  df-2s 28570

This theorem is referenced by:  nohalf  28583  pw2recs  28597  halfcut  28617