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

Theorem negsunif 28102
Description: Uniformity property for surreal negation. If 𝐿 and 𝑅 are any cut that represents 𝐴, then they may be used instead of ( L ‘𝐴) and ( R ‘𝐴) in the definition of negation. (Contributed by Scott Fenton, 14-Feb-2025.)
Hypotheses
Ref Expression
negsunif.1 (𝜑𝐿 <<s 𝑅)
negsunif.2 (𝜑𝐴 = (𝐿 |s 𝑅))
Assertion
Ref Expression
negsunif (𝜑 → ( -us𝐴) = (( -us𝑅) |s ( -us𝐿)))

Proof of Theorem negsunif
Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 negsunif.2 . . . 4 (𝜑𝐴 = (𝐿 |s 𝑅))
2 negsunif.1 . . . . 5 (𝜑𝐿 <<s 𝑅)
32scutcld 27863 . . . 4 (𝜑 → (𝐿 |s 𝑅) ∈ No )
41, 3eqeltrd 2839 . . 3 (𝜑𝐴 No )
5 negsval 28072 . . 3 (𝐴 No → ( -us𝐴) = (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴))))
64, 5syl 17 . 2 (𝜑 → ( -us𝐴) = (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴))))
7 negscut2 28087 . . . 4 (𝐴 No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
84, 7syl 17 . . 3 (𝜑 → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴)))
92, 1cofcutr2d 27975 . . . . 5 (𝜑 → ∀𝑐 ∈ ( R ‘𝐴)∃𝑑𝑅 𝑑 ≤s 𝑐)
10 negsfn 28070 . . . . . . . 8 -us Fn No
11 ssltss2 27849 . . . . . . . . 9 (𝐿 <<s 𝑅𝑅 No )
122, 11syl 17 . . . . . . . 8 (𝜑𝑅 No )
13 breq2 5152 . . . . . . . . 9 (𝑏 = ( -us𝑑) → (( -us𝑐) ≤s 𝑏 ↔ ( -us𝑐) ≤s ( -us𝑑)))
1413rexima 7258 . . . . . . . 8 (( -us Fn No 𝑅 No ) → (∃𝑏 ∈ ( -us𝑅)( -us𝑐) ≤s 𝑏 ↔ ∃𝑑𝑅 ( -us𝑐) ≤s ( -us𝑑)))
1510, 12, 14sylancr 587 . . . . . . 7 (𝜑 → (∃𝑏 ∈ ( -us𝑅)( -us𝑐) ≤s 𝑏 ↔ ∃𝑑𝑅 ( -us𝑐) ≤s ( -us𝑑)))
1615ralbidv 3176 . . . . . 6 (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us𝑅)( -us𝑐) ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑𝑅 ( -us𝑐) ≤s ( -us𝑑)))
1712adantr 480 . . . . . . . . . 10 ((𝜑𝑐 ∈ ( R ‘𝐴)) → 𝑅 No )
1817sselda 3995 . . . . . . . . 9 (((𝜑𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑𝑅) → 𝑑 No )
19 rightssno 27935 . . . . . . . . . . 11 ( R ‘𝐴) ⊆ No
2019sseli 3991 . . . . . . . . . 10 (𝑐 ∈ ( R ‘𝐴) → 𝑐 No )
2120ad2antlr 727 . . . . . . . . 9 (((𝜑𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑𝑅) → 𝑐 No )
2218, 21slenegd 28095 . . . . . . . 8 (((𝜑𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑𝑅) → (𝑑 ≤s 𝑐 ↔ ( -us𝑐) ≤s ( -us𝑑)))
2322rexbidva 3175 . . . . . . 7 ((𝜑𝑐 ∈ ( R ‘𝐴)) → (∃𝑑𝑅 𝑑 ≤s 𝑐 ↔ ∃𝑑𝑅 ( -us𝑐) ≤s ( -us𝑑)))
2423ralbidva 3174 . . . . . 6 (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑑𝑅 𝑑 ≤s 𝑐 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑𝑅 ( -us𝑐) ≤s ( -us𝑑)))
2516, 24bitr4d 282 . . . . 5 (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us𝑅)( -us𝑐) ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑𝑅 𝑑 ≤s 𝑐))
269, 25mpbird 257 . . . 4 (𝜑 → ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us𝑅)( -us𝑐) ≤s 𝑏)
27 breq1 5151 . . . . . . 7 (𝑎 = ( -us𝑐) → (𝑎 ≤s 𝑏 ↔ ( -us𝑐) ≤s 𝑏))
2827rexbidv 3177 . . . . . 6 (𝑎 = ( -us𝑐) → (∃𝑏 ∈ ( -us𝑅)𝑎 ≤s 𝑏 ↔ ∃𝑏 ∈ ( -us𝑅)( -us𝑐) ≤s 𝑏))
2928ralima 7257 . . . . 5 (( -us Fn No ∧ ( R ‘𝐴) ⊆ No ) → (∀𝑎 ∈ ( -us “ ( R ‘𝐴))∃𝑏 ∈ ( -us𝑅)𝑎 ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us𝑅)( -us𝑐) ≤s 𝑏))
3010, 19, 29mp2an 692 . . . 4 (∀𝑎 ∈ ( -us “ ( R ‘𝐴))∃𝑏 ∈ ( -us𝑅)𝑎 ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us𝑅)( -us𝑐) ≤s 𝑏)
3126, 30sylibr 234 . . 3 (𝜑 → ∀𝑎 ∈ ( -us “ ( R ‘𝐴))∃𝑏 ∈ ( -us𝑅)𝑎 ≤s 𝑏)
322, 1cofcutr1d 27974 . . . . 5 (𝜑 → ∀𝑐 ∈ ( L ‘𝐴)∃𝑑𝐿 𝑐 ≤s 𝑑)
33 ssltss1 27848 . . . . . . . . 9 (𝐿 <<s 𝑅𝐿 No )
342, 33syl 17 . . . . . . . 8 (𝜑𝐿 No )
35 breq1 5151 . . . . . . . . 9 (𝑏 = ( -us𝑑) → (𝑏 ≤s ( -us𝑐) ↔ ( -us𝑑) ≤s ( -us𝑐)))
3635rexima 7258 . . . . . . . 8 (( -us Fn No 𝐿 No ) → (∃𝑏 ∈ ( -us𝐿)𝑏 ≤s ( -us𝑐) ↔ ∃𝑑𝐿 ( -us𝑑) ≤s ( -us𝑐)))
3710, 34, 36sylancr 587 . . . . . . 7 (𝜑 → (∃𝑏 ∈ ( -us𝐿)𝑏 ≤s ( -us𝑐) ↔ ∃𝑑𝐿 ( -us𝑑) ≤s ( -us𝑐)))
3837ralbidv 3176 . . . . . 6 (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us𝐿)𝑏 ≤s ( -us𝑐) ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑𝐿 ( -us𝑑) ≤s ( -us𝑐)))
39 leftssno 27934 . . . . . . . . . . 11 ( L ‘𝐴) ⊆ No
4039sseli 3991 . . . . . . . . . 10 (𝑐 ∈ ( L ‘𝐴) → 𝑐 No )
4140ad2antlr 727 . . . . . . . . 9 (((𝜑𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑𝐿) → 𝑐 No )
4234adantr 480 . . . . . . . . . 10 ((𝜑𝑐 ∈ ( L ‘𝐴)) → 𝐿 No )
4342sselda 3995 . . . . . . . . 9 (((𝜑𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑𝐿) → 𝑑 No )
4441, 43slenegd 28095 . . . . . . . 8 (((𝜑𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑𝐿) → (𝑐 ≤s 𝑑 ↔ ( -us𝑑) ≤s ( -us𝑐)))
4544rexbidva 3175 . . . . . . 7 ((𝜑𝑐 ∈ ( L ‘𝐴)) → (∃𝑑𝐿 𝑐 ≤s 𝑑 ↔ ∃𝑑𝐿 ( -us𝑑) ≤s ( -us𝑐)))
4645ralbidva 3174 . . . . . 6 (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑑𝐿 𝑐 ≤s 𝑑 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑𝐿 ( -us𝑑) ≤s ( -us𝑐)))
4738, 46bitr4d 282 . . . . 5 (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us𝐿)𝑏 ≤s ( -us𝑐) ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑𝐿 𝑐 ≤s 𝑑))
4832, 47mpbird 257 . . . 4 (𝜑 → ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us𝐿)𝑏 ≤s ( -us𝑐))
49 breq2 5152 . . . . . . 7 (𝑎 = ( -us𝑐) → (𝑏 ≤s 𝑎𝑏 ≤s ( -us𝑐)))
5049rexbidv 3177 . . . . . 6 (𝑎 = ( -us𝑐) → (∃𝑏 ∈ ( -us𝐿)𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ( -us𝐿)𝑏 ≤s ( -us𝑐)))
5150ralima 7257 . . . . 5 (( -us Fn No ∧ ( L ‘𝐴) ⊆ No ) → (∀𝑎 ∈ ( -us “ ( L ‘𝐴))∃𝑏 ∈ ( -us𝐿)𝑏 ≤s 𝑎 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us𝐿)𝑏 ≤s ( -us𝑐)))
5210, 39, 51mp2an 692 . . . 4 (∀𝑎 ∈ ( -us “ ( L ‘𝐴))∃𝑏 ∈ ( -us𝐿)𝑏 ≤s 𝑎 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us𝐿)𝑏 ≤s ( -us𝑐))
5348, 52sylibr 234 . . 3 (𝜑 → ∀𝑎 ∈ ( -us “ ( L ‘𝐴))∃𝑏 ∈ ( -us𝐿)𝑏 ≤s 𝑎)
54 fnfun 6669 . . . . . . 7 ( -us Fn No → Fun -us )
5510, 54ax-mp 5 . . . . . 6 Fun -us
56 ssltex2 27847 . . . . . . 7 (𝐿 <<s 𝑅𝑅 ∈ V)
572, 56syl 17 . . . . . 6 (𝜑𝑅 ∈ V)
58 funimaexg 6654 . . . . . 6 ((Fun -us𝑅 ∈ V) → ( -us𝑅) ∈ V)
5955, 57, 58sylancr 587 . . . . 5 (𝜑 → ( -us𝑅) ∈ V)
60 snex 5442 . . . . . 6 {( -us𝐴)} ∈ V
6160a1i 11 . . . . 5 (𝜑 → {( -us𝐴)} ∈ V)
62 imassrn 6091 . . . . . . 7 ( -us𝑅) ⊆ ran -us
63 negsfo 28100 . . . . . . . 8 -us : No onto No
64 forn 6824 . . . . . . . 8 ( -us : No onto No → ran -us = No )
6563, 64ax-mp 5 . . . . . . 7 ran -us = No
6662, 65sseqtri 4032 . . . . . 6 ( -us𝑅) ⊆ No
6766a1i 11 . . . . 5 (𝜑 → ( -us𝑅) ⊆ No )
684negscld 28084 . . . . . 6 (𝜑 → ( -us𝐴) ∈ No )
6968snssd 4814 . . . . 5 (𝜑 → {( -us𝐴)} ⊆ No )
70 velsn 4647 . . . . . . . 8 (𝑎 ∈ {( -us𝐴)} ↔ 𝑎 = ( -us𝐴))
71 fvelimab 6981 . . . . . . . . . . 11 (( -us Fn No 𝑅 No ) → (𝑏 ∈ ( -us𝑅) ↔ ∃𝑑𝑅 ( -us𝑑) = 𝑏))
7210, 12, 71sylancr 587 . . . . . . . . . 10 (𝜑 → (𝑏 ∈ ( -us𝑅) ↔ ∃𝑑𝑅 ( -us𝑑) = 𝑏))
731sneqd 4643 . . . . . . . . . . . . . . . 16 (𝜑 → {𝐴} = {(𝐿 |s 𝑅)})
7473adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑑𝑅) → {𝐴} = {(𝐿 |s 𝑅)})
75 scutcut 27861 . . . . . . . . . . . . . . . . . 18 (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
762, 75syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 |s 𝑅) ∈ No 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
7776simp3d 1143 . . . . . . . . . . . . . . . 16 (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅)
7877adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑑𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅)
7974, 78eqbrtrd 5170 . . . . . . . . . . . . . 14 ((𝜑𝑑𝑅) → {𝐴} <<s 𝑅)
80 snidg 4665 . . . . . . . . . . . . . . . 16 (𝐴 No 𝐴 ∈ {𝐴})
814, 80syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ {𝐴})
8281adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑑𝑅) → 𝐴 ∈ {𝐴})
83 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑑𝑅) → 𝑑𝑅)
8479, 82, 83ssltsepcd 27854 . . . . . . . . . . . . 13 ((𝜑𝑑𝑅) → 𝐴 <s 𝑑)
854adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑑𝑅) → 𝐴 No )
8612sselda 3995 . . . . . . . . . . . . . 14 ((𝜑𝑑𝑅) → 𝑑 No )
8785, 86sltnegd 28094 . . . . . . . . . . . . 13 ((𝜑𝑑𝑅) → (𝐴 <s 𝑑 ↔ ( -us𝑑) <s ( -us𝐴)))
8884, 87mpbid 232 . . . . . . . . . . . 12 ((𝜑𝑑𝑅) → ( -us𝑑) <s ( -us𝐴))
89 breq1 5151 . . . . . . . . . . . 12 (( -us𝑑) = 𝑏 → (( -us𝑑) <s ( -us𝐴) ↔ 𝑏 <s ( -us𝐴)))
9088, 89syl5ibcom 245 . . . . . . . . . . 11 ((𝜑𝑑𝑅) → (( -us𝑑) = 𝑏𝑏 <s ( -us𝐴)))
9190rexlimdva 3153 . . . . . . . . . 10 (𝜑 → (∃𝑑𝑅 ( -us𝑑) = 𝑏𝑏 <s ( -us𝐴)))
9272, 91sylbid 240 . . . . . . . . 9 (𝜑 → (𝑏 ∈ ( -us𝑅) → 𝑏 <s ( -us𝐴)))
93 breq2 5152 . . . . . . . . . 10 (𝑎 = ( -us𝐴) → (𝑏 <s 𝑎𝑏 <s ( -us𝐴)))
9493imbi2d 340 . . . . . . . . 9 (𝑎 = ( -us𝐴) → ((𝑏 ∈ ( -us𝑅) → 𝑏 <s 𝑎) ↔ (𝑏 ∈ ( -us𝑅) → 𝑏 <s ( -us𝐴))))
9592, 94syl5ibrcom 247 . . . . . . . 8 (𝜑 → (𝑎 = ( -us𝐴) → (𝑏 ∈ ( -us𝑅) → 𝑏 <s 𝑎)))
9670, 95biimtrid 242 . . . . . . 7 (𝜑 → (𝑎 ∈ {( -us𝐴)} → (𝑏 ∈ ( -us𝑅) → 𝑏 <s 𝑎)))
97963imp 1110 . . . . . 6 ((𝜑𝑎 ∈ {( -us𝐴)} ∧ 𝑏 ∈ ( -us𝑅)) → 𝑏 <s 𝑎)
98973com23 1125 . . . . 5 ((𝜑𝑏 ∈ ( -us𝑅) ∧ 𝑎 ∈ {( -us𝐴)}) → 𝑏 <s 𝑎)
9959, 61, 67, 69, 98ssltd 27851 . . . 4 (𝜑 → ( -us𝑅) <<s {( -us𝐴)})
1006sneqd 4643 . . . 4 (𝜑 → {( -us𝐴)} = {(( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴)))})
10199, 100breqtrd 5174 . . 3 (𝜑 → ( -us𝑅) <<s {(( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴)))})
102 ssltex1 27846 . . . . . . 7 (𝐿 <<s 𝑅𝐿 ∈ V)
1032, 102syl 17 . . . . . 6 (𝜑𝐿 ∈ V)
104 funimaexg 6654 . . . . . 6 ((Fun -us𝐿 ∈ V) → ( -us𝐿) ∈ V)
10555, 103, 104sylancr 587 . . . . 5 (𝜑 → ( -us𝐿) ∈ V)
106 imassrn 6091 . . . . . . 7 ( -us𝐿) ⊆ ran -us
107106, 65sseqtri 4032 . . . . . 6 ( -us𝐿) ⊆ No
108107a1i 11 . . . . 5 (𝜑 → ( -us𝐿) ⊆ No )
109 fvelimab 6981 . . . . . . . . . 10 (( -us Fn No 𝐿 No ) → (𝑏 ∈ ( -us𝐿) ↔ ∃𝑐𝐿 ( -us𝑐) = 𝑏))
11010, 34, 109sylancr 587 . . . . . . . . 9 (𝜑 → (𝑏 ∈ ( -us𝐿) ↔ ∃𝑐𝐿 ( -us𝑐) = 𝑏))
1112adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝐿) → 𝐿 <<s 𝑅)
112111, 75syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝐿) → ((𝐿 |s 𝑅) ∈ No 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅))
113112simp2d 1142 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)})
11473adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐𝐿) → {𝐴} = {(𝐿 |s 𝑅)})
115113, 114breqtrrd 5176 . . . . . . . . . . . . 13 ((𝜑𝑐𝐿) → 𝐿 <<s {𝐴})
116 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑐𝐿) → 𝑐𝐿)
11781adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐𝐿) → 𝐴 ∈ {𝐴})
118115, 116, 117ssltsepcd 27854 . . . . . . . . . . . 12 ((𝜑𝑐𝐿) → 𝑐 <s 𝐴)
11934sselda 3995 . . . . . . . . . . . . 13 ((𝜑𝑐𝐿) → 𝑐 No )
1204adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐𝐿) → 𝐴 No )
121119, 120sltnegd 28094 . . . . . . . . . . . 12 ((𝜑𝑐𝐿) → (𝑐 <s 𝐴 ↔ ( -us𝐴) <s ( -us𝑐)))
122118, 121mpbid 232 . . . . . . . . . . 11 ((𝜑𝑐𝐿) → ( -us𝐴) <s ( -us𝑐))
123 breq2 5152 . . . . . . . . . . 11 (( -us𝑐) = 𝑏 → (( -us𝐴) <s ( -us𝑐) ↔ ( -us𝐴) <s 𝑏))
124122, 123syl5ibcom 245 . . . . . . . . . 10 ((𝜑𝑐𝐿) → (( -us𝑐) = 𝑏 → ( -us𝐴) <s 𝑏))
125124rexlimdva 3153 . . . . . . . . 9 (𝜑 → (∃𝑐𝐿 ( -us𝑐) = 𝑏 → ( -us𝐴) <s 𝑏))
126110, 125sylbid 240 . . . . . . . 8 (𝜑 → (𝑏 ∈ ( -us𝐿) → ( -us𝐴) <s 𝑏))
127 breq1 5151 . . . . . . . . 9 (𝑎 = ( -us𝐴) → (𝑎 <s 𝑏 ↔ ( -us𝐴) <s 𝑏))
128127imbi2d 340 . . . . . . . 8 (𝑎 = ( -us𝐴) → ((𝑏 ∈ ( -us𝐿) → 𝑎 <s 𝑏) ↔ (𝑏 ∈ ( -us𝐿) → ( -us𝐴) <s 𝑏)))
129126, 128syl5ibrcom 247 . . . . . . 7 (𝜑 → (𝑎 = ( -us𝐴) → (𝑏 ∈ ( -us𝐿) → 𝑎 <s 𝑏)))
13070, 129biimtrid 242 . . . . . 6 (𝜑 → (𝑎 ∈ {( -us𝐴)} → (𝑏 ∈ ( -us𝐿) → 𝑎 <s 𝑏)))
1311303imp 1110 . . . . 5 ((𝜑𝑎 ∈ {( -us𝐴)} ∧ 𝑏 ∈ ( -us𝐿)) → 𝑎 <s 𝑏)
13261, 105, 69, 108, 131ssltd 27851 . . . 4 (𝜑 → {( -us𝐴)} <<s ( -us𝐿))
133100, 132eqbrtrrd 5172 . . 3 (𝜑 → {(( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴)))} <<s ( -us𝐿))
1348, 31, 53, 101, 133cofcut1d 27970 . 2 (𝜑 → (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴))) = (( -us𝑅) |s ( -us𝐿)))
1356, 134eqtrd 2775 1 (𝜑 → ( -us𝐴) = (( -us𝑅) |s ( -us𝐿)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wral 3059  wrex 3068  Vcvv 3478  wss 3963  {csn 4631   class class class wbr 5148  ran crn 5690  cima 5692  Fun wfun 6557   Fn wfn 6558  ontowfo 6561  cfv 6563  (class class class)co 7431   No csur 27699   <s cslt 27700   ≤s csle 27804   <<s csslt 27840   |s cscut 27842   L cleft 27899   R cright 27900   -us cnegs 28066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-ot 4640  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-1o 8505  df-2o 8506  df-nadd 8703  df-no 27702  df-slt 27703  df-bday 27704  df-sle 27805  df-sslt 27841  df-scut 27843  df-0s 27884  df-made 27901  df-old 27902  df-left 27904  df-right 27905  df-norec 27986  df-norec2 27997  df-adds 28008  df-negs 28068
This theorem is referenced by:  zscut  28408  renegscl  28445
  Copyright terms: Public domain W3C validator