MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nohalf Structured version   Visualization version   GIF version

Theorem nohalf 28407
Description: An explicit expression for one half. This theorem avoids the axiom of infinity. (Contributed by Scott Fenton, 23-Jul-2025.)
Assertion
Ref Expression
nohalf ( 1s /su 2s) = ({ 0s } |s { 1s })

Proof of Theorem nohalf
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 5436 . . . . . . . 8 { 0s } ∈ V
21a1i 11 . . . . . . 7 (⊤ → { 0s } ∈ V)
3 snex 5436 . . . . . . . 8 { 1s } ∈ V
43a1i 11 . . . . . . 7 (⊤ → { 1s } ∈ V)
5 0sno 27871 . . . . . . . . 9 0s No
65a1i 11 . . . . . . . 8 (⊤ → 0s No )
76snssd 4809 . . . . . . 7 (⊤ → { 0s } ⊆ No )
8 1sno 27872 . . . . . . . 8 1s No
9 snssi 4808 . . . . . . . 8 ( 1s No → { 1s } ⊆ No )
108, 9mp1i 13 . . . . . . 7 (⊤ → { 1s } ⊆ No )
11 velsn 4642 . . . . . . . . 9 (𝑥 ∈ { 0s } ↔ 𝑥 = 0s )
12 velsn 4642 . . . . . . . . 9 (𝑦 ∈ { 1s } ↔ 𝑦 = 1s )
13 0slt1s 27874 . . . . . . . . . 10 0s <s 1s
14 breq12 5148 . . . . . . . . . 10 ((𝑥 = 0s𝑦 = 1s ) → (𝑥 <s 𝑦 ↔ 0s <s 1s ))
1513, 14mpbiri 258 . . . . . . . . 9 ((𝑥 = 0s𝑦 = 1s ) → 𝑥 <s 𝑦)
1611, 12, 15syl2anb 598 . . . . . . . 8 ((𝑥 ∈ { 0s } ∧ 𝑦 ∈ { 1s }) → 𝑥 <s 𝑦)
17163adant1 1131 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ { 0s } ∧ 𝑦 ∈ { 1s }) → 𝑥 <s 𝑦)
182, 4, 7, 10, 17ssltd 27836 . . . . . 6 (⊤ → { 0s } <<s { 1s })
1918scutcld 27848 . . . . 5 (⊤ → ({ 0s } |s { 1s }) ∈ No )
2019mptru 1547 . . . 4 ({ 0s } |s { 1s }) ∈ No
21 no2times 28401 . . . 4 (({ 0s } |s { 1s }) ∈ No → (2s ·s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })))
2220, 21ax-mp 5 . . 3 (2s ·s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s }))
23 eqidd 2738 . . . . . 6 (⊤ → ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))
2418, 18, 23, 23addsunif 28035 . . . . 5 (⊤ → (({ 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 𝑦)})))
2524mptru 1547 . . . 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 𝑦)}))
265elexi 3503 . . . . . . . . . . 11 0s ∈ V
27 oveq1 7438 . . . . . . . . . . . . 13 (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ( 0s +s ({ 0s } |s { 1s })))
28 addslid 28001 . . . . . . . . . . . . . 14 (({ 0s } |s { 1s }) ∈ No → ( 0s +s ({ 0s } |s { 1s })) = ({ 0s } |s { 1s }))
2920, 28ax-mp 5 . . . . . . . . . . . . 13 ( 0s +s ({ 0s } |s { 1s })) = ({ 0s } |s { 1s })
3027, 29eqtrdi 2793 . . . . . . . . . . . 12 (𝑦 = 0s → (𝑦 +s ({ 0s } |s { 1s })) = ({ 0s } |s { 1s }))
3130eqeq2d 2748 . . . . . . . . . . 11 (𝑦 = 0s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s })))
3226, 31rexsn 4682 . . . . . . . . . 10 (∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s }))
3332abbii 2809 . . . . . . . . 9 {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥𝑥 = ({ 0s } |s { 1s })}
34 df-sn 4627 . . . . . . . . 9 {({ 0s } |s { 1s })} = {𝑥𝑥 = ({ 0s } |s { 1s })}
3533, 34eqtr4i 2768 . . . . . . . 8 {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {({ 0s } |s { 1s })}
36 oveq2 7439 . . . . . . . . . . . . 13 (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 0s ))
37 addsrid 27997 . . . . . . . . . . . . . 14 (({ 0s } |s { 1s }) ∈ No → (({ 0s } |s { 1s }) +s 0s ) = ({ 0s } |s { 1s }))
3820, 37ax-mp 5 . . . . . . . . . . . . 13 (({ 0s } |s { 1s }) +s 0s ) = ({ 0s } |s { 1s })
3936, 38eqtrdi 2793 . . . . . . . . . . . 12 (𝑦 = 0s → (({ 0s } |s { 1s }) +s 𝑦) = ({ 0s } |s { 1s }))
4039eqeq2d 2748 . . . . . . . . . . 11 (𝑦 = 0s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s })))
4126, 40rexsn 4682 . . . . . . . . . 10 (∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s }))
4241abbii 2809 . . . . . . . . 9 {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥𝑥 = ({ 0s } |s { 1s })}
4342, 34eqtr4i 2768 . . . . . . . 8 {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {({ 0s } |s { 1s })}
4435, 43uneq12i 4166 . . . . . . 7 ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })})
45 unidm 4157 . . . . . . 7 ({({ 0s } |s { 1s })} ∪ {({ 0s } |s { 1s })}) = {({ 0s } |s { 1s })}
4644, 45eqtri 2765 . . . . . 6 ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {({ 0s } |s { 1s })}
478elexi 3503 . . . . . . . . . . 11 1s ∈ V
48 oveq1 7438 . . . . . . . . . . . . 13 (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = ( 1s +s ({ 0s } |s { 1s })))
49 addscom 27999 . . . . . . . . . . . . . 14 (( 1s No ∧ ({ 0s } |s { 1s }) ∈ No ) → ( 1s +s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s 1s ))
508, 20, 49mp2an 692 . . . . . . . . . . . . 13 ( 1s +s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s 1s )
5148, 50eqtrdi 2793 . . . . . . . . . . . 12 (𝑦 = 1s → (𝑦 +s ({ 0s } |s { 1s })) = (({ 0s } |s { 1s }) +s 1s ))
5251eqeq2d 2748 . . . . . . . . . . 11 (𝑦 = 1s → (𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
5347, 52rexsn 4682 . . . . . . . . . 10 (∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s })) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
5453abbii 2809 . . . . . . . . 9 {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {𝑥𝑥 = (({ 0s } |s { 1s }) +s 1s )}
55 df-sn 4627 . . . . . . . . 9 {(({ 0s } |s { 1s }) +s 1s )} = {𝑥𝑥 = (({ 0s } |s { 1s }) +s 1s )}
5654, 55eqtr4i 2768 . . . . . . . 8 {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} = {(({ 0s } |s { 1s }) +s 1s )}
57 oveq2 7439 . . . . . . . . . . . 12 (𝑦 = 1s → (({ 0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s }) +s 1s ))
5857eqeq2d 2748 . . . . . . . . . . 11 (𝑦 = 1s → (𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s )))
5947, 58rexsn 4682 . . . . . . . . . 10 (∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s }) +s 1s ))
6059abbii 2809 . . . . . . . . 9 {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {𝑥𝑥 = (({ 0s } |s { 1s }) +s 1s )}
6160, 55eqtr4i 2768 . . . . . . . 8 {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)} = {(({ 0s } |s { 1s }) +s 1s )}
6256, 61uneq12i 4166 . . . . . . 7 ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = ({(({ 0s } |s { 1s }) +s 1s )} ∪ {(({ 0s } |s { 1s }) +s 1s )})
63 unidm 4157 . . . . . . 7 ({(({ 0s } |s { 1s }) +s 1s )} ∪ {(({ 0s } |s { 1s }) +s 1s )}) = {(({ 0s } |s { 1s }) +s 1s )}
6462, 63eqtri 2765 . . . . . 6 ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) = {(({ 0s } |s { 1s }) +s 1s )}
6546, 64oveq12i 7443 . . . . 5 (({𝑥 ∣ ∃𝑦 ∈ { 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 {(({ 0s } |s { 1s }) +s 1s )})
66 ral0 4513 . . . . . . 7 𝑥 ∈ ∅ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) <s 𝑥
67 slerflex 27808 . . . . . . . . . . . 12 ( 1s No → 1s ≤s 1s )
688, 67ax-mp 5 . . . . . . . . . . 11 1s ≤s 1s
69 breq1 5146 . . . . . . . . . . . 12 (𝑦 = 1s → (𝑦 ≤s 1s ↔ 1s ≤s 1s ))
7047, 69rexsn 4682 . . . . . . . . . . 11 (∃𝑦 ∈ { 1s }𝑦 ≤s 1s ↔ 1s ≤s 1s )
7168, 70mpbir 231 . . . . . . . . . 10 𝑦 ∈ { 1s }𝑦 ≤s 1s
7271olci 867 . . . . . . . . 9 (∃𝑥 ∈ { 0s } ({ 0s } |s { 1s }) ≤s 𝑥 ∨ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s )
7318mptru 1547 . . . . . . . . . 10 { 0s } <<s { 1s }
74 snelpwi 5448 . . . . . . . . . . . 12 ( 0s No → { 0s } ∈ 𝒫 No )
755, 74ax-mp 5 . . . . . . . . . . 11 { 0s } ∈ 𝒫 No
76 nulssgt 27843 . . . . . . . . . . 11 ({ 0s } ∈ 𝒫 No → { 0s } <<s ∅)
7775, 76ax-mp 5 . . . . . . . . . 10 { 0s } <<s ∅
78 eqid 2737 . . . . . . . . . 10 ({ 0s } |s { 1s }) = ({ 0s } |s { 1s })
79 df-1s 27870 . . . . . . . . . 10 1s = ({ 0s } |s ∅)
80 sltrec 27865 . . . . . . . . . 10 ((({ 0s } <<s { 1s } ∧ { 0s } <<s ∅) ∧ (({ 0s } |s { 1s }) = ({ 0s } |s { 1s }) ∧ 1s = ({ 0s } |s ∅))) → (({ 0s } |s { 1s }) <s 1s ↔ (∃𝑥 ∈ { 0s } ({ 0s } |s { 1s }) ≤s 𝑥 ∨ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s )))
8173, 77, 78, 79, 80mp4an 693 . . . . . . . . 9 (({ 0s } |s { 1s }) <s 1s ↔ (∃𝑥 ∈ { 0s } ({ 0s } |s { 1s }) ≤s 𝑥 ∨ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s ))
8272, 81mpbir 231 . . . . . . . 8 ({ 0s } |s { 1s }) <s 1s
83 ovex 7464 . . . . . . . . 9 ({ 0s } |s { 1s }) ∈ V
84 breq1 5146 . . . . . . . . 9 (𝑦 = ({ 0s } |s { 1s }) → (𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s ))
8583, 84ralsn 4681 . . . . . . . 8 (∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s ↔ ({ 0s } |s { 1s }) <s 1s )
8682, 85mpbir 231 . . . . . . 7 𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s
87 snex 5436 . . . . . . . . . . 11 {({ 0s } |s { 1s })} ∈ V
8887a1i 11 . . . . . . . . . 10 (⊤ → {({ 0s } |s { 1s })} ∈ V)
89 snex 5436 . . . . . . . . . . 11 {(({ 0s } |s { 1s }) +s 1s )} ∈ V
9089a1i 11 . . . . . . . . . 10 (⊤ → {(({ 0s } |s { 1s }) +s 1s )} ∈ V)
9119snssd 4809 . . . . . . . . . 10 (⊤ → {({ 0s } |s { 1s })} ⊆ No )
928a1i 11 . . . . . . . . . . . 12 (⊤ → 1s No )
9319, 92addscld 28013 . . . . . . . . . . 11 (⊤ → (({ 0s } |s { 1s }) +s 1s ) ∈ No )
9493snssd 4809 . . . . . . . . . 10 (⊤ → {(({ 0s } |s { 1s }) +s 1s )} ⊆ No )
95 velsn 4642 . . . . . . . . . . . 12 (𝑥 ∈ {({ 0s } |s { 1s })} ↔ 𝑥 = ({ 0s } |s { 1s }))
96 velsn 4642 . . . . . . . . . . . 12 (𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )} ↔ 𝑦 = (({ 0s } |s { 1s }) +s 1s ))
97 sltadd2 28024 . . . . . . . . . . . . . . . 16 (( 0s No ∧ 1s No ∧ ({ 0s } |s { 1s }) ∈ No ) → ( 0s <s 1s ↔ (({ 0s } |s { 1s }) +s 0s ) <s (({ 0s } |s { 1s }) +s 1s )))
985, 8, 20, 97mp3an 1463 . . . . . . . . . . . . . . 15 ( 0s <s 1s ↔ (({ 0s } |s { 1s }) +s 0s ) <s (({ 0s } |s { 1s }) +s 1s ))
9913, 98mpbi 230 . . . . . . . . . . . . . 14 (({ 0s } |s { 1s }) +s 0s ) <s (({ 0s } |s { 1s }) +s 1s )
10038, 99eqbrtrri 5166 . . . . . . . . . . . . 13 ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s )
101 breq12 5148 . . . . . . . . . . . . 13 ((𝑥 = ({ 0s } |s { 1s }) ∧ 𝑦 = (({ 0s } |s { 1s }) +s 1s )) → (𝑥 <s 𝑦 ↔ ({ 0s } |s { 1s }) <s (({ 0s } |s { 1s }) +s 1s )))
102100, 101mpbiri 258 . . . . . . . . . . . 12 ((𝑥 = ({ 0s } |s { 1s }) ∧ 𝑦 = (({ 0s } |s { 1s }) +s 1s )) → 𝑥 <s 𝑦)
10395, 96, 102syl2anb 598 . . . . . . . . . . 11 ((𝑥 ∈ {({ 0s } |s { 1s })} ∧ 𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )}) → 𝑥 <s 𝑦)
1041033adant1 1131 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ {({ 0s } |s { 1s })} ∧ 𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )}) → 𝑥 <s 𝑦)
10588, 90, 91, 94, 104ssltd 27836 . . . . . . . . 9 (⊤ → {({ 0s } |s { 1s })} <<s {(({ 0s } |s { 1s }) +s 1s )})
106105mptru 1547 . . . . . . . 8 {({ 0s } |s { 1s })} <<s {(({ 0s } |s { 1s }) +s 1s )}
107 eqid 2737 . . . . . . . 8 ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})
108 slerec 27864 . . . . . . . 8 ((({({ 0s } |s { 1s })} <<s {(({ 0s } |s { 1s }) +s 1s )} ∧ { 0s } <<s ∅) ∧ (({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ∧ 1s = ({ 0s } |s ∅))) → (({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ≤s 1s ↔ (∀𝑥 ∈ ∅ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) <s 𝑥 ∧ ∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s )))
109106, 77, 107, 79, 108mp4an 693 . . . . . . 7 (({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ≤s 1s ↔ (∀𝑥 ∈ ∅ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) <s 𝑥 ∧ ∀𝑦 ∈ {({ 0s } |s { 1s })}𝑦 <s 1s ))
11066, 86, 109mpbir2an 711 . . . . . 6 ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ≤s 1s
111 addslid 28001 . . . . . . . . . 10 ( 1s No → ( 0s +s 1s ) = 1s )
1128, 111ax-mp 5 . . . . . . . . 9 ( 0s +s 1s ) = 1s
113 slerflex 27808 . . . . . . . . . . . . . 14 ( 0s No → 0s ≤s 0s )
1145, 113ax-mp 5 . . . . . . . . . . . . 13 0s ≤s 0s
115 breq2 5147 . . . . . . . . . . . . . 14 (𝑥 = 0s → ( 0s ≤s 𝑥 ↔ 0s ≤s 0s ))
11626, 115rexsn 4682 . . . . . . . . . . . . 13 (∃𝑥 ∈ { 0s } 0s ≤s 𝑥 ↔ 0s ≤s 0s )
117114, 116mpbir 231 . . . . . . . . . . . 12 𝑥 ∈ { 0s } 0s ≤s 𝑥
118117orci 866 . . . . . . . . . . 11 (∃𝑥 ∈ { 0s } 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({ 0s } |s { 1s }))
119 0elpw 5356 . . . . . . . . . . . . 13 ∅ ∈ 𝒫 No
120 nulssgt 27843 . . . . . . . . . . . . 13 (∅ ∈ 𝒫 No → ∅ <<s ∅)
121119, 120ax-mp 5 . . . . . . . . . . . 12 ∅ <<s ∅
122 df-0s 27869 . . . . . . . . . . . 12 0s = (∅ |s ∅)
123 sltrec 27865 . . . . . . . . . . . 12 (((∅ <<s ∅ ∧ { 0s } <<s { 1s }) ∧ ( 0s = (∅ |s ∅) ∧ ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))) → ( 0s <s ({ 0s } |s { 1s }) ↔ (∃𝑥 ∈ { 0s } 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({ 0s } |s { 1s }))))
124121, 73, 122, 78, 123mp4an 693 . . . . . . . . . . 11 ( 0s <s ({ 0s } |s { 1s }) ↔ (∃𝑥 ∈ { 0s } 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({ 0s } |s { 1s })))
125118, 124mpbir 231 . . . . . . . . . 10 0s <s ({ 0s } |s { 1s })
126 sltadd1 28025 . . . . . . . . . . 11 (( 0s No ∧ ({ 0s } |s { 1s }) ∈ No ∧ 1s No ) → ( 0s <s ({ 0s } |s { 1s }) ↔ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s )))
1275, 20, 8, 126mp3an 1463 . . . . . . . . . 10 ( 0s <s ({ 0s } |s { 1s }) ↔ ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s ))
128125, 127mpbi 230 . . . . . . . . 9 ( 0s +s 1s ) <s (({ 0s } |s { 1s }) +s 1s )
129112, 128eqbrtrri 5166 . . . . . . . 8 1s <s (({ 0s } |s { 1s }) +s 1s )
130 ovex 7464 . . . . . . . . 9 (({ 0s } |s { 1s }) +s 1s ) ∈ V
131 breq2 5147 . . . . . . . . 9 (𝑦 = (({ 0s } |s { 1s }) +s 1s ) → ( 1s <s 𝑦 ↔ 1s <s (({ 0s } |s { 1s }) +s 1s )))
132130, 131ralsn 4681 . . . . . . . 8 (∀𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )} 1s <s 𝑦 ↔ 1s <s (({ 0s } |s { 1s }) +s 1s ))
133129, 132mpbir 231 . . . . . . 7 𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )} 1s <s 𝑦
134 breq2 5147 . . . . . . . . . . . . . 14 (𝑥 = 1s → ( 0s <s 𝑥 ↔ 0s <s 1s ))
13547, 134ralsn 4681 . . . . . . . . . . . . 13 (∀𝑥 ∈ { 1s } 0s <s 𝑥 ↔ 0s <s 1s )
13613, 135mpbir 231 . . . . . . . . . . . 12 𝑥 ∈ { 1s } 0s <s 𝑥
137 ral0 4513 . . . . . . . . . . . 12 𝑦 ∈ ∅ 𝑦 <s ({ 0s } |s { 1s })
138 slerec 27864 . . . . . . . . . . . . 13 (((∅ <<s ∅ ∧ { 0s } <<s { 1s }) ∧ ( 0s = (∅ |s ∅) ∧ ({ 0s } |s { 1s }) = ({ 0s } |s { 1s }))) → ( 0s ≤s ({ 0s } |s { 1s }) ↔ (∀𝑥 ∈ { 1s } 0s <s 𝑥 ∧ ∀𝑦 ∈ ∅ 𝑦 <s ({ 0s } |s { 1s }))))
139121, 73, 122, 78, 138mp4an 693 . . . . . . . . . . . 12 ( 0s ≤s ({ 0s } |s { 1s }) ↔ (∀𝑥 ∈ { 1s } 0s <s 𝑥 ∧ ∀𝑦 ∈ ∅ 𝑦 <s ({ 0s } |s { 1s })))
140136, 137, 139mpbir2an 711 . . . . . . . . . . 11 0s ≤s ({ 0s } |s { 1s })
141 breq2 5147 . . . . . . . . . . . 12 (𝑥 = ({ 0s } |s { 1s }) → ( 0s ≤s 𝑥 ↔ 0s ≤s ({ 0s } |s { 1s })))
14283, 141rexsn 4682 . . . . . . . . . . 11 (∃𝑥 ∈ {({ 0s } |s { 1s })} 0s ≤s 𝑥 ↔ 0s ≤s ({ 0s } |s { 1s }))
143140, 142mpbir 231 . . . . . . . . . 10 𝑥 ∈ {({ 0s } |s { 1s })} 0s ≤s 𝑥
144143orci 866 . . . . . . . . 9 (∃𝑥 ∈ {({ 0s } |s { 1s })} 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}))
145 sltrec 27865 . . . . . . . . . 10 (((∅ <<s ∅ ∧ {({ 0s } |s { 1s })} <<s {(({ 0s } |s { 1s }) +s 1s )}) ∧ ( 0s = (∅ |s ∅) ∧ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}))) → ( 0s <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ↔ (∃𝑥 ∈ {({ 0s } |s { 1s })} 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}))))
146121, 106, 122, 107, 145mp4an 693 . . . . . . . . 9 ( 0s <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ↔ (∃𝑥 ∈ {({ 0s } |s { 1s })} 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})))
147144, 146mpbir 231 . . . . . . . 8 0s <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})
148 breq1 5146 . . . . . . . . 9 (𝑥 = 0s → (𝑥 <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ↔ 0s <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})))
14926, 148ralsn 4681 . . . . . . . 8 (∀𝑥 ∈ { 0s }𝑥 <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ↔ 0s <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}))
150147, 149mpbir 231 . . . . . . 7 𝑥 ∈ { 0s }𝑥 <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})
151 slerec 27864 . . . . . . . 8 ((({ 0s } <<s ∅ ∧ {({ 0s } |s { 1s })} <<s {(({ 0s } |s { 1s }) +s 1s )}) ∧ ( 1s = ({ 0s } |s ∅) ∧ ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}))) → ( 1s ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ↔ (∀𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )} 1s <s 𝑦 ∧ ∀𝑥 ∈ { 0s }𝑥 <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}))))
15277, 106, 79, 107, 151mp4an 693 . . . . . . 7 ( 1s ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ↔ (∀𝑦 ∈ {(({ 0s } |s { 1s }) +s 1s )} 1s <s 𝑦 ∧ ∀𝑥 ∈ { 0s }𝑥 <s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})))
153133, 150, 152mpbir2an 711 . . . . . 6 1s ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})
154105scutcld 27848 . . . . . . . 8 (⊤ → ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ∈ No )
155154mptru 1547 . . . . . . 7 ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ∈ No
156 sletri3 27800 . . . . . . 7 ((({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ∈ No ∧ 1s No ) → (({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = 1s ↔ (({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ≤s 1s ∧ 1s ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}))))
157155, 8, 156mp2an 692 . . . . . 6 (({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = 1s ↔ (({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) ≤s 1s ∧ 1s ≤s ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )})))
158110, 153, 157mpbir2an 711 . . . . 5 ({({ 0s } |s { 1s })} |s {(({ 0s } |s { 1s }) +s 1s )}) = 1s
15965, 158eqtri 2765 . . . 4 (({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s { 1s }) +s 𝑦)})) = 1s
16025, 159eqtri 2765 . . 3 (({ 0s } |s { 1s }) +s ({ 0s } |s { 1s })) = 1s
16122, 160eqtri 2765 . 2 (2s ·s ({ 0s } |s { 1s })) = 1s
162 2sno 28403 . . . . 5 2s No
163 2ne0s 28404 . . . . 5 2s ≠ 0s
164162, 163pm3.2i 470 . . . 4 (2s No ∧ 2s ≠ 0s )
1658, 20, 1643pm3.2i 1340 . . 3 ( 1s No ∧ ({ 0s } |s { 1s }) ∈ No ∧ (2s No ∧ 2s ≠ 0s ))
166 oveq2 7439 . . . . . 6 (𝑥 = ({ 0s } |s { 1s }) → (2s ·s 𝑥) = (2s ·s ({ 0s } |s { 1s })))
167166eqeq1d 2739 . . . . 5 (𝑥 = ({ 0s } |s { 1s }) → ((2s ·s 𝑥) = 1s ↔ (2s ·s ({ 0s } |s { 1s })) = 1s ))
168167rspcev 3622 . . . 4 ((({ 0s } |s { 1s }) ∈ No ∧ (2s ·s ({ 0s } |s { 1s })) = 1s ) → ∃𝑥 No (2s ·s 𝑥) = 1s )
16920, 161, 168mp2an 692 . . 3 𝑥 No (2s ·s 𝑥) = 1s
170 divsmulw 28218 . . 3 ((( 1s No ∧ ({ 0s } |s { 1s }) ∈ No ∧ (2s No ∧ 2s ≠ 0s )) ∧ ∃𝑥 No (2s ·s 𝑥) = 1s ) → (( 1s /su 2s) = ({ 0s } |s { 1s }) ↔ (2s ·s ({ 0s } |s { 1s })) = 1s ))
171165, 169, 170mp2an 692 . 2 (( 1s /su 2s) = ({ 0s } |s { 1s }) ↔ (2s ·s ({ 0s } |s { 1s })) = 1s )
172161, 171mpbir 231 1 ( 1s /su 2s) = ({ 0s } |s { 1s })
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wtru 1541  wcel 2108  {cab 2714  wne 2940  wral 3061  wrex 3070  Vcvv 3480  cun 3949  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626   class class class wbr 5143  (class class class)co 7431   No csur 27684   <s cslt 27685   ≤s csle 27789   <<s csslt 27825   |s cscut 27827   0s c0s 27867   1s c1s 27868   +s cadds 27992   ·s cmuls 28132   /su cdivs 28213  2sc2s 28394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-nadd 8704  df-no 27687  df-slt 27688  df-bday 27689  df-sle 27790  df-sslt 27826  df-scut 27828  df-0s 27869  df-1s 27870  df-made 27886  df-old 27887  df-left 27889  df-right 27890  df-norec 27971  df-norec2 27982  df-adds 27993  df-negs 28053  df-subs 28054  df-muls 28133  df-divs 28214  df-n0s 28320  df-nns 28321  df-2s 28395
This theorem is referenced by:  cutpw2  28417
  Copyright terms: Public domain W3C validator