Theorem twocut 28686

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 28072	. . . . . . 7 ⊢ 0s ∈ No
2	1	a1i 11	. . . . . 6 ⊢ (⊤ → 0s ∈ No )
3		1no 28073	. . . . . . 7 ⊢ 1s ∈ No
4	3	a1i 11	. . . . . 6 ⊢ (⊤ → 1s ∈ No )
5		0lt1s 28075	. . . . . . 7 ⊢ 0s <s 1s
6	5	a1i 11	. . . . . 6 ⊢ (⊤ → 0s <s 1s )
7	2, 4, 6	sltssn 28033	. . . . 5 ⊢ (⊤ → { 0s } <<s { 1s })
8	7	cutscld 28046	. . . 4 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ No )
9	8	mptru 1577	. . 3 ⊢ ({ 0s } |s { 1s }) ∈ No
10		no2times 28680	. . 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 2763	. . . . 5 ⊢ (⊤ → ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))
13	7, 7, 12, 12	addsunif 28265	. . . 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 3475	. . . . . . . . . . 11 ⊢ 0s ∈ V
16		oveq1 7423	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ( 0s +s ({ 0s } |s { 1s })))
17	16	eqeq2d 2773	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s }))))
18	15, 17	rexsn 4646	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s })))
19		addslid 28231	. . . . . . . . . . . 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 2775	. . . . . . . . . 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 2829	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
24		df-sn 4588	. . . . . . . 8 ⊢ {({ 0s } |s { 1s })} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
25	23, 24	eqtr4i 2788	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {({ 0s } |s { 1s })}
26		oveq2 7424	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 0s ))
27	26	eqeq2d 2773	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s )))
28	15, 27	rexsn 4646	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s ))
29		addsrid 28227	. . . . . . . . . . . 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 2775	. . . . . . . . . 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 2829	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
34	33, 24	eqtr4i 2788	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {({ 0s } |s { 1s })}
35	25, 34	uneq12i 4116	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })})
36		unidm 4107	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })}) = {({ 0s } |s { 1s })}
37	35, 36	eqtri 2785	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {({ 0s } |s { 1s })}
38	3	elexi 3475	. . . . . . . . . 10 ⊢ 1s ∈ V
39		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = ( 1s +s ({ 0s } |s { 1s })))
40	39	eqeq2d 2773	. . . . . . . . . 10 ⊢ (𝑦 = 1s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))))
41	38, 40	rexsn 4646	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
42	41	abbii 2829	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
43		df-sn 4588	. . . . . . . 8 ⊢ {( 1s +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
44	42, 43	eqtr4i 2788	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {( 1s +s ({ 0s } |s { 1s }))}
45		oveq2 7424	. . . . . . . . . . . 12 ⊢ (𝑦 = 1s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 1s ))
46	45	eqeq2d 2773	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
47	38, 46	rexsn 4646	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
48		addscom 28229	. . . . . . . . . . . 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 2775	. . . . . . . . . 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 2829	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
53	52, 43	eqtr4i 2788	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {( 1s +s ({ 0s } |s { 1s }))}
54	44, 53	uneq12i 4116	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))})
55		unidm 4107	. . . . . 6 ⊢ ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))}) = {( 1s +s ({ 0s } |s { 1s }))}
56	54, 55	eqtri 2785	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {( 1s +s ({ 0s } |s { 1s }))}
57	37, 56	oveq12i 7428	. . . 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 28044	. . . . . . . . . . 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 7449	. . . . . . . . . . 11 ⊢ ({ 0s } |s { 1s }) ∈ V
63	62	snid 4626	. . . . . . . . . 10 ⊢ ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })}
64	63	a1i 11	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })})
65	38	snid 4626	. . . . . . . . . 10 ⊢ 1s ∈ { 1s }
66	65	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 1s ∈ { 1s })
67	61, 64, 66	sltssepcd 28035	. . . . . . . 8 ⊢ (⊤ → ({ 0s } |s { 1s }) <s 1s )
68	67	mptru 1577	. . . . . . 7 ⊢ ({ 0s } |s { 1s }) <s 1s
69		breq1 5110	. . . . . . . 8 ⊢ (𝑦 = ({ 0s } |s { 1s }) → (𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s ))
70	62, 69	ralsn 4645	. . . . . . 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 28243	. . . . . . . . 9 ⊢ (⊤ → ( 1s +s ({ 0s } |s { 1s })) ∈ No )
73	8	ltsp1d 28278	. . . . . . . . . 10 ⊢ (⊤ → ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s ))
74	73, 49	breqtrdi 5150	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ( 1s +s ({ 0s } |s { 1s })))
75	8, 72, 74	sltssn 28033	. . . . . . . 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 5423	. . . . . . . . 9 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
78	1, 77	ax-mp 5	. . . . . . . 8 ⊢ { 0s } ∈ 𝒫 No
79		nulsgts 28039	. . . . . . . 8 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
80	78, 79	ax-mp 5	. . . . . . 7 ⊢ { 0s } <<s ∅
81		eqid 2762	. . . . . . 7 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
82		df-1s 28071	. . . . . . 7 ⊢ 1s = ({ 0s } |s ∅)
83		lesrec 28062	. . . . . . 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 4626	. . . . . . . . . . . 12 ⊢ 0s ∈ { 0s }
88	87	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 0s ∈ { 0s })
89	86, 88, 64	sltssepcd 28035	. . . . . . . . . 10 ⊢ (⊤ → 0s <s ({ 0s } |s { 1s }))
90	89	mptru 1577	. . . . . . . . 9 ⊢ 0s <s ({ 0s } |s { 1s })
91		ltadds1 28255	. . . . . . . . . 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 1490	. . . . . . . . 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 28231	. . . . . . . . 9 ⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
95	3, 94	ax-mp 5	. . . . . . . 8 ⊢ ( 0s +s 1s ) = 1s
96	93, 95, 49	3brtr3i 5138	. . . . . . 7 ⊢ 1s <s ( 1s +s ({ 0s } |s { 1s }))
97		ovex 7449	. . . . . . . 8 ⊢ ( 1s +s ({ 0s } |s { 1s })) ∈ V
98		breq2 5111	. . . . . . . 8 ⊢ (𝑥 = ( 1s +s ({ 0s } |s { 1s })) → ( 1s <s 𝑥 ↔ 1s <s ( 1s +s ({ 0s } |s { 1s }))))
99	97, 98	ralsn 4645	. . . . . . 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 28046	. . . . . . . . 9 ⊢ (⊤ → ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No )
102		cutcuts 28044	. . . . . . . . . . . 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 7449	. . . . . . . . . . . 12 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ V
106	105	snid 4626	. . . . . . . . . . 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 28035	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
109	2, 8, 101, 89, 108	ltstrd 27997	. . . . . . . 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 5110	. . . . . . . 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 4645	. . . . . . 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 28062	. . . . . . 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 27989	. . . . . 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 2785	. . 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 2785	. 2 ⊢ (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })) = 1s
123	11, 122	eqtri 2785	1 ⊢ (2s ·s ({ 0s } |s { 1s })) = 1s

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145  {cab 2740  ∀wral 3078  ∃wrex 3088   ∪ cun 3900  ∅c0 4282  𝒫 cpw 4560  {csn 4587   class class class wbr 5107  (class class class)co 7416   No csur 27874   <s clts 27875   ≤s cles 27978   <<s cslts 28020   |s ccuts 28022   0_s c0s 28068   1_s c1s 28069   +_s cadds 28222   ·_s cmuls 28369  2_sc2s 28673

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-ot 4596  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  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 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-2o 8459  df-nadd 8657  df-no 27877  df-lts 27878  df-bday 27879  df-les 27979  df-slts 28021  df-cuts 28023  df-0s 28070  df-1s 28071  df-made 28090  df-old 28091  df-left 28093  df-right 28094  df-norec 28201  df-norec2 28212  df-adds 28223  df-negs 28284  df-subs 28285  df-muls 28370  df-n0s 28577  df-2s 28674

This theorem is used by:  nohalf  28687  pw2recs  28701  halfcut  28721