Theorem twocut 28346

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		0sno 27770	. . . . . . 7 ⊢ 0s ∈ No
2	1	a1i 11	. . . . . 6 ⊢ (⊤ → 0s ∈ No )
3		1sno 27771	. . . . . . 7 ⊢ 1s ∈ No
4	3	a1i 11	. . . . . 6 ⊢ (⊤ → 1s ∈ No )
5		0slt1s 27773	. . . . . . 7 ⊢ 0s <s 1s
6	5	a1i 11	. . . . . 6 ⊢ (⊤ → 0s <s 1s )
7	2, 4, 6	ssltsn 27733	. . . . 5 ⊢ (⊤ → { 0s } <<s { 1s })
8	7	scutcld 27744	. . . 4 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ No )
9	8	mptru 1548	. . 3 ⊢ ({ 0s } |s { 1s }) ∈ No
10		no2times 28340	. . 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 2732	. . . . 5 ⊢ (⊤ → ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))
13	7, 7, 12, 12	addsunif 27945	. . . 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 1548	. . 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 3459	. . . . . . . . . . 11 ⊢ 0s ∈ V
16		oveq1 7353	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ( 0s +s ({ 0s } |s { 1s })))
17	16	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s }))))
18	15, 17	rexsn 4632	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 0s +s ({ 0s } |s { 1s })))
19		addslid 27911	. . . . . . . . . . . 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 2744	. . . . . . . . . 10 ⊢ (𝑥 = ( 0s +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s }))
22	18, 21	bitri 275	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s }))
23	22	abbii 2798	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
24		df-sn 4574	. . . . . . . 8 ⊢ {({ 0s } |s { 1s })} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
25	23, 24	eqtr4i 2757	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {({ 0s } |s { 1s })}
26		oveq2 7354	. . . . . . . . . . . 12 ⊢ (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 0s ))
27	26	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑦 = 0s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s )))
28	15, 27	rexsn 4632	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 0s ))
29		addsrid 27907	. . . . . . . . . . . 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 2744	. . . . . . . . . 10 ⊢ (𝑥 = (({ 0s } |s { 1s }) +s 0s ) ↔ 𝑥 = ({ 0s } |s { 1s }))
32	28, 31	bitri 275	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s }))
33	32	abbii 2798	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s })}
34	33, 24	eqtr4i 2757	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {({ 0s } |s { 1s })}
35	25, 34	uneq12i 4113	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })})
36		unidm 4104	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })}) = {({ 0s } |s { 1s })}
37	35, 36	eqtri 2754	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {({ 0s } |s { 1s })}
38	3	elexi 3459	. . . . . . . . . 10 ⊢ 1s ∈ V
39		oveq1 7353	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = ( 1s +s ({ 0s } |s { 1s })))
40	39	eqeq2d 2742	. . . . . . . . . 10 ⊢ (𝑦 = 1s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))))
41	38, 40	rexsn 4632	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
42	41	abbii 2798	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
43		df-sn 4574	. . . . . . . 8 ⊢ {( 1s +s ({ 0s } |s { 1s }))} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
44	42, 43	eqtr4i 2757	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {( 1s +s ({ 0s } |s { 1s }))}
45		oveq2 7354	. . . . . . . . . . . 12 ⊢ (𝑦 = 1s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 1s ))
46	45	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑦 = 1s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
47	38, 46	rexsn 4632	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
48		addscom 27909	. . . . . . . . . . . 12 ⊢ ((({ 0s } |s { 1s }) ∈ No ∧ 1s ∈ No ) → (({ 0s } |s { 1s }) +s 1s ) = ( 1s +s ({ 0s } |s { 1s })))
49	9, 3, 48	mp2an 692	. . . . . . . . . . 11 ⊢ (({ 0s } |s { 1s }) +s 1s ) = ( 1s +s ({ 0s } |s { 1s }))
50	49	eqeq2i 2744	. . . . . . . . . 10 ⊢ (𝑥 = (({ 0s } |s { 1s }) +s 1s ) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
51	47, 50	bitri 275	. . . . . . . . 9 ⊢ (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ( 1s +s ({ 0s } |s { 1s })))
52	51	abbii 2798	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ( 1s +s ({ 0s } |s { 1s }))}
53	52, 43	eqtr4i 2757	. . . . . . 7 ⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {( 1s +s ({ 0s } |s { 1s }))}
54	44, 53	uneq12i 4113	. . . . . 6 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))})
55		unidm 4104	. . . . . 6 ⊢ ({( 1s +s ({ 0s } |s { 1s }))} ∪ {( 1s +s ({ 0s } |s { 1s }))}) = {( 1s +s ({ 0s } |s { 1s }))}
56	54, 55	eqtri 2754	. . . . 5 ⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {( 1s +s ({ 0s } |s { 1s }))}
57	37, 56	oveq12i 7358	. . . 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 4460	. . . . . 6 ⊢ ∀𝑥 ∈ ∅ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) <s 𝑥
59		scutcut 27742	. . . . . . . . . . 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 1144	. . . . . . . . 9 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s { 1s })
62		ovex 7379	. . . . . . . . . . 11 ⊢ ({ 0s } |s { 1s }) ∈ V
63	62	snid 4612	. . . . . . . . . 10 ⊢ ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })}
64	63	a1i 11	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) ∈ {({ 0s } |s { 1s })})
65	38	snid 4612	. . . . . . . . . 10 ⊢ 1s ∈ { 1s }
66	65	a1i 11	. . . . . . . . 9 ⊢ (⊤ → 1s ∈ { 1s })
67	61, 64, 66	ssltsepcd 27735	. . . . . . . 8 ⊢ (⊤ → ({ 0s } |s { 1s }) <s 1s )
68	67	mptru 1548	. . . . . . 7 ⊢ ({ 0s } |s { 1s }) <s 1s
69		breq1 5092	. . . . . . . 8 ⊢ (𝑦 = ({ 0s } |s { 1s }) → (𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s ))
70	62, 69	ralsn 4631	. . . . . . 7 ⊢ (∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s )
71	68, 70	mpbir 231	. . . . . 6 ⊢ ∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s
72	4, 8	addscld 27923	. . . . . . . . 9 ⊢ (⊤ → ( 1s +s ({ 0s } |s { 1s })) ∈ No )
73	8	sltp1d 27958	. . . . . . . . . 10 ⊢ (⊤ → ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s ))
74	73, 49	breqtrdi 5130	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ( 1s +s ({ 0s } |s { 1s })))
75	8, 72, 74	ssltsn 27733	. . . . . . . 8 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {( 1s +s ({ 0s } |s { 1s }))})
76	75	mptru 1548	. . . . . . 7 ⊢ {({ 0s } |s { 1s })} <<s {( 1s +s ({ 0s } |s { 1s }))}
77		snelpwi 5383	. . . . . . . . 9 ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
78	1, 77	ax-mp 5	. . . . . . . 8 ⊢ { 0s } ∈ 𝒫 No
79		nulssgt 27739	. . . . . . . 8 ⊢ ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
80	78, 79	ax-mp 5	. . . . . . 7 ⊢ { 0s } <<s ∅
81		eqid 2731	. . . . . . 7 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
82		df-1s 27769	. . . . . . 7 ⊢ 1s = ({ 0s } |s ∅)
83		slerec 27760	. . . . . . 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 693	. . . . . 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 711	. . . . 5 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ≤s 1s
86	60	simp2d 1143	. . . . . . . . . . 11 ⊢ (⊤ → { 0s } <<s {({ 0s } |s { 1s })})
87	15	snid 4612	. . . . . . . . . . . 12 ⊢ 0s ∈ { 0s }
88	87	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 0s ∈ { 0s })
89	86, 88, 64	ssltsepcd 27735	. . . . . . . . . 10 ⊢ (⊤ → 0s <s ({ 0s } |s { 1s }))
90	89	mptru 1548	. . . . . . . . 9 ⊢ 0s <s ({ 0s } |s { 1s })
91		sltadd1 27935	. . . . . . . . . 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 1463	. . . . . . . . 9 ⊢ ( 0s <s ({ 0s } |s { 1s }) ↔ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s ))
93	90, 92	mpbi 230	. . . . . . . 8 ⊢ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s )
94		addslid 27911	. . . . . . . . 9 ⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
95	3, 94	ax-mp 5	. . . . . . . 8 ⊢ ( 0s +s 1s ) = 1s
96	93, 95, 49	3brtr3i 5118	. . . . . . 7 ⊢ 1s <s ( 1s +s ({ 0s } |s { 1s }))
97		ovex 7379	. . . . . . . 8 ⊢ ( 1s +s ({ 0s } |s { 1s })) ∈ V
98		breq2 5093	. . . . . . . 8 ⊢ (𝑥 = ( 1s +s ({ 0s } |s { 1s })) → ( 1s <s 𝑥 ↔ 1s <s ( 1s +s ({ 0s } |s { 1s }))))
99	97, 98	ralsn 4631	. . . . . . 7 ⊢ (∀𝑥 ∈ {( 1s +s ({ 0s } |s { 1s }))} 1s <s 𝑥 ↔ 1s <s ( 1s +s ({ 0s } |s { 1s })))
100	96, 99	mpbir 231	. . . . . 6 ⊢ ∀𝑥 ∈ {( 1s +s ({ 0s } |s { 1s }))} 1s <s 𝑥
101	75	scutcld 27744	. . . . . . . . 9 ⊢ (⊤ → ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No )
102		scutcut 27742	. . . . . . . . . . . 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 1143	. . . . . . . . . 10 ⊢ (⊤ → {({ 0s } |s { 1s })} <<s {({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})})
105		ovex 7379	. . . . . . . . . . . 12 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ V
106	105	snid 4612	. . . . . . . . . . 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	ssltsepcd 27735	. . . . . . . . 9 ⊢ (⊤ → ({ 0s } |s { 1s }) <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
109	2, 8, 101, 89, 108	slttrd 27698	. . . . . . . 8 ⊢ (⊤ → 0s <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}))
110	109	mptru 1548	. . . . . . 7 ⊢ 0s <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
111		breq1 5092	. . . . . . . 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 4631	. . . . . . 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 231	. . . . . 6 ⊢ ∀𝑦 ∈ { 0s }𝑦 <s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
114		slerec 27760	. . . . . . 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 693	. . . . . 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 711	. . . . 5 ⊢ 1s ≤s ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))})
117	101	mptru 1548	. . . . . 6 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) ∈ No
118		sletri3 27694	. . . . . 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 692	. . . . 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 711	. . . 4 ⊢ ({({ 0s } |s { 1s })} |s {( 1s +s ({ 0s } |s { 1s }))}) = 1s
121	57, 120	eqtri 2754	. . 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 2754	. 2 ⊢ (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })) = 1s
123	11, 122	eqtri 2754	1 ⊢ (2s ·s ({ 0s } |s { 1s })) = 1s

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ⊤wtru 1542   ∈ wcel 2111  {cab 2709  ∀wral 3047  ∃wrex 3056   ∪ cun 3895  ∅c0 4280  𝒫 cpw 4547  {csn 4573   class class class wbr 5089  (class class class)co 7346   No csur 27578   <s cslt 27579   ≤s csle 27683   <<s csslt 27720   |s cscut 27722   0_s c0s 27766   1_s c1s 27767   +_s cadds 27902   ·_s cmuls 28045  2_sc2s 28333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-ot 4582  df-uni 4857  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-se 5568  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-1o 8385  df-2o 8386  df-nadd 8581  df-no 27581  df-slt 27582  df-bday 27583  df-sle 27684  df-sslt 27721  df-scut 27723  df-0s 27768  df-1s 27769  df-made 27788  df-old 27789  df-left 27791  df-right 27792  df-norec 27881  df-norec2 27892  df-adds 27903  df-negs 27963  df-subs 27964  df-muls 28046  df-2s 28334

This theorem is referenced by:  nohalf  28347  pw2recs  28361  halfcut  28378