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

Theorem negsunif 27871
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 27640 . . . 4 (𝜑 → (ðŋ |s 𝑅) ∈ No )
41, 3eqeltrd 2825 . . 3 (𝜑 → ðī ∈ No )
5 negsval 27842 . . 3 (ðī ∈ No → ( -us ‘ðī) = (( -us “ ( R ‘ðī)) |s ( -us “ ( L ‘ðī))))
64, 5syl 17 . 2 (𝜑 → ( -us ‘ðī) = (( -us “ ( R ‘ðī)) |s ( -us “ ( L ‘ðī))))
7 negscut2 27856 . . . 4 (ðī ∈ No → ( -us “ ( R ‘ðī)) <<s ( -us “ ( L ‘ðī)))
84, 7syl 17 . . 3 (𝜑 → ( -us “ ( R ‘ðī)) <<s ( -us “ ( L ‘ðī)))
92, 1cofcutr2d 27750 . . . . 5 (𝜑 → ∀𝑐 ∈ ( R ‘ðī)∃𝑑 ∈ 𝑅 𝑑 â‰Īs 𝑐)
10 negsfn 27840 . . . . . . . 8 -us Fn No
11 ssltss2 27626 . . . . . . . . 9 (ðŋ <<s 𝑅 → 𝑅 ⊆ No )
122, 11syl 17 . . . . . . . 8 (𝜑 → 𝑅 ⊆ No )
13 breq2 5142 . . . . . . . . 9 (𝑏 = ( -us ‘𝑑) → (( -us ‘𝑐) â‰Īs 𝑏 ↔ ( -us ‘𝑐) â‰Īs ( -us ‘𝑑)))
1413imaeqsexv 7352 . . . . . . . 8 (( -us Fn No ∧ 𝑅 ⊆ No ) → (∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) â‰Īs 𝑏 ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑐) â‰Īs ( -us ‘𝑑)))
1510, 12, 14sylancr 586 . . . . . . 7 (𝜑 → (∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) â‰Īs 𝑏 ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑐) â‰Īs ( -us ‘𝑑)))
1615ralbidv 3169 . . . . . 6 (𝜑 → (∀𝑐 ∈ ( R ‘ðī)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) â‰Īs 𝑏 ↔ ∀𝑐 ∈ ( R ‘ðī)∃𝑑 ∈ 𝑅 ( -us ‘𝑐) â‰Īs ( -us ‘𝑑)))
1712adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 𝑐 ∈ ( R ‘ðī)) → 𝑅 ⊆ No )
1817sselda 3974 . . . . . . . . 9 (((𝜑 ∧ 𝑐 ∈ ( R ‘ðī)) ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈ No )
19 rightssno 27712 . . . . . . . . . . 11 ( R ‘ðī) ⊆ No
2019sseli 3970 . . . . . . . . . 10 (𝑐 ∈ ( R ‘ðī) → 𝑐 ∈ No )
2120ad2antlr 724 . . . . . . . . 9 (((𝜑 ∧ 𝑐 ∈ ( R ‘ðī)) ∧ 𝑑 ∈ 𝑅) → 𝑐 ∈ No )
2218, 21slenegd 27864 . . . . . . . 8 (((𝜑 ∧ 𝑐 ∈ ( R ‘ðī)) ∧ 𝑑 ∈ 𝑅) → (𝑑 â‰Īs 𝑐 ↔ ( -us ‘𝑐) â‰Īs ( -us ‘𝑑)))
2322rexbidva 3168 . . . . . . 7 ((𝜑 ∧ 𝑐 ∈ ( R ‘ðī)) → (∃𝑑 ∈ 𝑅 𝑑 â‰Īs 𝑐 ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑐) â‰Īs ( -us ‘𝑑)))
2423ralbidva 3167 . . . . . 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 5141 . . . . . . 7 (𝑎 = ( -us ‘𝑐) → (𝑎 â‰Īs 𝑏 ↔ ( -us ‘𝑐) â‰Īs 𝑏))
2827rexbidv 3170 . . . . . 6 (𝑎 = ( -us ‘𝑐) → (∃𝑏 ∈ ( -us “ 𝑅)𝑎 â‰Īs 𝑏 ↔ ∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) â‰Īs 𝑏))
2928imaeqsalv 7353 . . . . 5 (( -us Fn No ∧ ( R ‘ðī) ⊆ No ) → (∀𝑎 ∈ ( -us “ ( R ‘ðī))∃𝑏 ∈ ( -us “ 𝑅)𝑎 â‰Īs 𝑏 ↔ ∀𝑐 ∈ ( R ‘ðī)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) â‰Īs 𝑏))
3010, 19, 29mp2an 689 . . . 4 (∀𝑎 ∈ ( -us “ ( R ‘ðī))∃𝑏 ∈ ( -us “ 𝑅)𝑎 â‰Īs 𝑏 ↔ ∀𝑐 ∈ ( R ‘ðī)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) â‰Īs 𝑏)
3126, 30sylibr 233 . . 3 (𝜑 → ∀𝑎 ∈ ( -us “ ( R ‘ðī))∃𝑏 ∈ ( -us “ 𝑅)𝑎 â‰Īs 𝑏)
322, 1cofcutr1d 27749 . . . . 5 (𝜑 → ∀𝑐 ∈ ( L ‘ðī)∃𝑑 ∈ ðŋ 𝑐 â‰Īs 𝑑)
33 ssltss1 27625 . . . . . . . . 9 (ðŋ <<s 𝑅 → ðŋ ⊆ No )
342, 33syl 17 . . . . . . . 8 (𝜑 → ðŋ ⊆ No )
35 breq1 5141 . . . . . . . . 9 (𝑏 = ( -us ‘𝑑) → (𝑏 â‰Īs ( -us ‘𝑐) ↔ ( -us ‘𝑑) â‰Īs ( -us ‘𝑐)))
3635imaeqsexv 7352 . . . . . . . 8 (( -us Fn No ∧ ðŋ ⊆ No ) → (∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs ( -us ‘𝑐) ↔ ∃𝑑 ∈ ðŋ ( -us ‘𝑑) â‰Īs ( -us ‘𝑐)))
3710, 34, 36sylancr 586 . . . . . . 7 (𝜑 → (∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs ( -us ‘𝑐) ↔ ∃𝑑 ∈ ðŋ ( -us ‘𝑑) â‰Īs ( -us ‘𝑐)))
3837ralbidv 3169 . . . . . 6 (𝜑 → (∀𝑐 ∈ ( L ‘ðī)∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs ( -us ‘𝑐) ↔ ∀𝑐 ∈ ( L ‘ðī)∃𝑑 ∈ ðŋ ( -us ‘𝑑) â‰Īs ( -us ‘𝑐)))
39 leftssno 27711 . . . . . . . . . . 11 ( L ‘ðī) ⊆ No
4039sseli 3970 . . . . . . . . . 10 (𝑐 ∈ ( L ‘ðī) → 𝑐 ∈ No )
4140ad2antlr 724 . . . . . . . . 9 (((𝜑 ∧ 𝑐 ∈ ( L ‘ðī)) ∧ 𝑑 ∈ ðŋ) → 𝑐 ∈ No )
4234adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 𝑐 ∈ ( L ‘ðī)) → ðŋ ⊆ No )
4342sselda 3974 . . . . . . . . 9 (((𝜑 ∧ 𝑐 ∈ ( L ‘ðī)) ∧ 𝑑 ∈ ðŋ) → 𝑑 ∈ No )
4441, 43slenegd 27864 . . . . . . . 8 (((𝜑 ∧ 𝑐 ∈ ( L ‘ðī)) ∧ 𝑑 ∈ ðŋ) → (𝑐 â‰Īs 𝑑 ↔ ( -us ‘𝑑) â‰Īs ( -us ‘𝑐)))
4544rexbidva 3168 . . . . . . 7 ((𝜑 ∧ 𝑐 ∈ ( L ‘ðī)) → (∃𝑑 ∈ ðŋ 𝑐 â‰Īs 𝑑 ↔ ∃𝑑 ∈ ðŋ ( -us ‘𝑑) â‰Īs ( -us ‘𝑐)))
4645ralbidva 3167 . . . . . 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 5142 . . . . . . 7 (𝑎 = ( -us ‘𝑐) → (𝑏 â‰Īs 𝑎 ↔ 𝑏 â‰Īs ( -us ‘𝑐)))
5049rexbidv 3170 . . . . . 6 (𝑎 = ( -us ‘𝑐) → (∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs 𝑎 ↔ ∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs ( -us ‘𝑐)))
5150imaeqsalv 7353 . . . . 5 (( -us Fn No ∧ ( L ‘ðī) ⊆ No ) → (∀𝑎 ∈ ( -us “ ( L ‘ðī))∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs 𝑎 ↔ ∀𝑐 ∈ ( L ‘ðī)∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs ( -us ‘𝑐)))
5210, 39, 51mp2an 689 . . . 4 (∀𝑎 ∈ ( -us “ ( L ‘ðī))∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs 𝑎 ↔ ∀𝑐 ∈ ( L ‘ðī)∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs ( -us ‘𝑐))
5348, 52sylibr 233 . . 3 (𝜑 → ∀𝑎 ∈ ( -us “ ( L ‘ðī))∃𝑏 ∈ ( -us “ ðŋ)𝑏 â‰Īs 𝑎)
54 fnfun 6639 . . . . . . 7 ( -us Fn No → Fun -us )
5510, 54ax-mp 5 . . . . . 6 Fun -us
56 ssltex2 27624 . . . . . . 7 (ðŋ <<s 𝑅 → 𝑅 ∈ V)
572, 56syl 17 . . . . . 6 (𝜑 → 𝑅 ∈ V)
58 funimaexg 6624 . . . . . 6 ((Fun -us ∧ 𝑅 ∈ V) → ( -us “ 𝑅) ∈ V)
5955, 57, 58sylancr 586 . . . . 5 (𝜑 → ( -us “ 𝑅) ∈ V)
60 snex 5421 . . . . . 6 {( -us ‘ðī)} ∈ V
6160a1i 11 . . . . 5 (𝜑 → {( -us ‘ðī)} ∈ V)
62 imassrn 6060 . . . . . . 7 ( -us “ 𝑅) ⊆ ran -us
63 negsfo 27869 . . . . . . . 8 -us : No –onto→ No
64 forn 6798 . . . . . . . 8 ( -us : No –onto→ No → ran -us = No )
6563, 64ax-mp 5 . . . . . . 7 ran -us = No
6662, 65sseqtri 4010 . . . . . 6 ( -us “ 𝑅) ⊆ No
6766a1i 11 . . . . 5 (𝜑 → ( -us “ 𝑅) ⊆ No )
684negscld 27853 . . . . . 6 (𝜑 → ( -us ‘ðī) ∈ No )
6968snssd 4804 . . . . 5 (𝜑 → {( -us ‘ðī)} ⊆ No )
70 velsn 4636 . . . . . . . 8 (𝑎 ∈ {( -us ‘ðī)} ↔ 𝑎 = ( -us ‘ðī))
71 fvelimab 6954 . . . . . . . . . . 11 (( -us Fn No ∧ 𝑅 ⊆ No ) → (𝑏 ∈ ( -us “ 𝑅) ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑑) = 𝑏))
7210, 12, 71sylancr 586 . . . . . . . . . 10 (𝜑 → (𝑏 ∈ ( -us “ 𝑅) ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑑) = 𝑏))
731sneqd 4632 . . . . . . . . . . . . . . . 16 (𝜑 → {ðī} = {(ðŋ |s 𝑅)})
7473adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑑 ∈ 𝑅) → {ðī} = {(ðŋ |s 𝑅)})
75 scutcut 27638 . . . . . . . . . . . . . . . . . 18 (ðŋ <<s 𝑅 → ((ðŋ |s 𝑅) ∈ No ∧ ðŋ <<s {(ðŋ |s 𝑅)} ∧ {(ðŋ |s 𝑅)} <<s 𝑅))
762, 75syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ðŋ |s 𝑅) ∈ No ∧ ðŋ <<s {(ðŋ |s 𝑅)} ∧ {(ðŋ |s 𝑅)} <<s 𝑅))
7776simp3d 1141 . . . . . . . . . . . . . . . 16 (𝜑 → {(ðŋ |s 𝑅)} <<s 𝑅)
7877adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑑 ∈ 𝑅) → {(ðŋ |s 𝑅)} <<s 𝑅)
7974, 78eqbrtrd 5160 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑑 ∈ 𝑅) → {ðī} <<s 𝑅)
80 snidg 4654 . . . . . . . . . . . . . . . 16 (ðī ∈ No → ðī ∈ {ðī})
814, 80syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ðī ∈ {ðī})
8281adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑑 ∈ 𝑅) → ðī ∈ {ðī})
83 simpr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈ 𝑅)
8479, 82, 83ssltsepcd 27631 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑑 ∈ 𝑅) → ðī <s 𝑑)
854adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑑 ∈ 𝑅) → ðī ∈ No )
8612sselda 3974 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈ No )
8785, 86sltnegd 27863 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑑 ∈ 𝑅) → (ðī <s 𝑑 ↔ ( -us ‘𝑑) <s ( -us ‘ðī)))
8884, 87mpbid 231 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑑 ∈ 𝑅) → ( -us ‘𝑑) <s ( -us ‘ðī))
89 breq1 5141 . . . . . . . . . . . 12 (( -us ‘𝑑) = 𝑏 → (( -us ‘𝑑) <s ( -us ‘ðī) ↔ 𝑏 <s ( -us ‘ðī)))
9088, 89syl5ibcom 244 . . . . . . . . . . 11 ((𝜑 ∧ 𝑑 ∈ 𝑅) → (( -us ‘𝑑) = 𝑏 → 𝑏 <s ( -us ‘ðī)))
9190rexlimdva 3147 . . . . . . . . . 10 (𝜑 → (∃𝑑 ∈ 𝑅 ( -us ‘𝑑) = 𝑏 → 𝑏 <s ( -us ‘ðī)))
9272, 91sylbid 239 . . . . . . . . 9 (𝜑 → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s ( -us ‘ðī)))
93 breq2 5142 . . . . . . . . . 10 (𝑎 = ( -us ‘ðī) → (𝑏 <s 𝑎 ↔ 𝑏 <s ( -us ‘ðī)))
9493imbi2d 340 . . . . . . . . 9 (𝑎 = ( -us ‘ðī) → ((𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎) ↔ (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s ( -us ‘ðī))))
9592, 94syl5ibrcom 246 . . . . . . . 8 (𝜑 → (𝑎 = ( -us ‘ðī) → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎)))
9670, 95biimtrid 241 . . . . . . 7 (𝜑 → (𝑎 ∈ {( -us ‘ðī)} → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎)))
97963imp 1108 . . . . . 6 ((𝜑 ∧ 𝑎 ∈ {( -us ‘ðī)} ∧ 𝑏 ∈ ( -us “ 𝑅)) → 𝑏 <s 𝑎)
98973com23 1123 . . . . 5 ((𝜑 ∧ 𝑏 ∈ ( -us “ 𝑅) ∧ 𝑎 ∈ {( -us ‘ðī)}) → 𝑏 <s 𝑎)
9959, 61, 67, 69, 98ssltd 27628 . . . 4 (𝜑 → ( -us “ 𝑅) <<s {( -us ‘ðī)})
1006sneqd 4632 . . . 4 (𝜑 → {( -us ‘ðī)} = {(( -us “ ( R ‘ðī)) |s ( -us “ ( L ‘ðī)))})
10199, 100breqtrd 5164 . . 3 (𝜑 → ( -us “ 𝑅) <<s {(( -us “ ( R ‘ðī)) |s ( -us “ ( L ‘ðī)))})
102 ssltex1 27623 . . . . . . 7 (ðŋ <<s 𝑅 → ðŋ ∈ V)
1032, 102syl 17 . . . . . 6 (𝜑 → ðŋ ∈ V)
104 funimaexg 6624 . . . . . 6 ((Fun -us ∧ ðŋ ∈ V) → ( -us “ ðŋ) ∈ V)
10555, 103, 104sylancr 586 . . . . 5 (𝜑 → ( -us “ ðŋ) ∈ V)
106 imassrn 6060 . . . . . . 7 ( -us “ ðŋ) ⊆ ran -us
107106, 65sseqtri 4010 . . . . . 6 ( -us “ ðŋ) ⊆ No
108107a1i 11 . . . . 5 (𝜑 → ( -us “ ðŋ) ⊆ No )
109 fvelimab 6954 . . . . . . . . . 10 (( -us Fn No ∧ ðŋ ⊆ No ) → (𝑏 ∈ ( -us “ ðŋ) ↔ ∃𝑐 ∈ ðŋ ( -us ‘𝑐) = 𝑏))
11010, 34, 109sylancr 586 . . . . . . . . 9 (𝜑 → (𝑏 ∈ ( -us “ ðŋ) ↔ ∃𝑐 ∈ ðŋ ( -us ‘𝑐) = 𝑏))
1112adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑐 ∈ ðŋ) → ðŋ <<s 𝑅)
112111, 75syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑐 ∈ ðŋ) → ((ðŋ |s 𝑅) ∈ No ∧ ðŋ <<s {(ðŋ |s 𝑅)} ∧ {(ðŋ |s 𝑅)} <<s 𝑅))
113112simp2d 1140 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑐 ∈ ðŋ) → ðŋ <<s {(ðŋ |s 𝑅)})
11473adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑐 ∈ ðŋ) → {ðī} = {(ðŋ |s 𝑅)})
115113, 114breqtrrd 5166 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑐 ∈ ðŋ) → ðŋ <<s {ðī})
116 simpr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑐 ∈ ðŋ) → 𝑐 ∈ ðŋ)
11781adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑐 ∈ ðŋ) → ðī ∈ {ðī})
118115, 116, 117ssltsepcd 27631 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑐 ∈ ðŋ) → 𝑐 <s ðī)
11934sselda 3974 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑐 ∈ ðŋ) → 𝑐 ∈ No )
1204adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑐 ∈ ðŋ) → ðī ∈ No )
121119, 120sltnegd 27863 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑐 ∈ ðŋ) → (𝑐 <s ðī ↔ ( -us ‘ðī) <s ( -us ‘𝑐)))
122118, 121mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ 𝑐 ∈ ðŋ) → ( -us ‘ðī) <s ( -us ‘𝑐))
123 breq2 5142 . . . . . . . . . . 11 (( -us ‘𝑐) = 𝑏 → (( -us ‘ðī) <s ( -us ‘𝑐) ↔ ( -us ‘ðī) <s 𝑏))
124122, 123syl5ibcom 244 . . . . . . . . . 10 ((𝜑 ∧ 𝑐 ∈ ðŋ) → (( -us ‘𝑐) = 𝑏 → ( -us ‘ðī) <s 𝑏))
125124rexlimdva 3147 . . . . . . . . 9 (𝜑 → (∃𝑐 ∈ ðŋ ( -us ‘𝑐) = 𝑏 → ( -us ‘ðī) <s 𝑏))
126110, 125sylbid 239 . . . . . . . 8 (𝜑 → (𝑏 ∈ ( -us “ ðŋ) → ( -us ‘ðī) <s 𝑏))
127 breq1 5141 . . . . . . . . 9 (𝑎 = ( -us ‘ðī) → (𝑎 <s 𝑏 ↔ ( -us ‘ðī) <s 𝑏))
128127imbi2d 340 . . . . . . . 8 (𝑎 = ( -us ‘ðī) → ((𝑏 ∈ ( -us “ ðŋ) → 𝑎 <s 𝑏) ↔ (𝑏 ∈ ( -us “ ðŋ) → ( -us ‘ðī) <s 𝑏)))
129126, 128syl5ibrcom 246 . . . . . . 7 (𝜑 → (𝑎 = ( -us ‘ðī) → (𝑏 ∈ ( -us “ ðŋ) → 𝑎 <s 𝑏)))
13070, 129biimtrid 241 . . . . . 6 (𝜑 → (𝑎 ∈ {( -us ‘ðī)} → (𝑏 ∈ ( -us “ ðŋ) → 𝑎 <s 𝑏)))
1311303imp 1108 . . . . 5 ((𝜑 ∧ 𝑎 ∈ {( -us ‘ðī)} ∧ 𝑏 ∈ ( -us “ ðŋ)) → 𝑎 <s 𝑏)
13261, 105, 69, 108, 131ssltd 27628 . . . 4 (𝜑 → {( -us ‘ðī)} <<s ( -us “ ðŋ))
133100, 132eqbrtrrd 5162 . . 3 (𝜑 → {(( -us “ ( R ‘ðī)) |s ( -us “ ( L ‘ðī)))} <<s ( -us “ ðŋ))
1348, 31, 53, 101, 133cofcut1d 27745 . 2 (𝜑 → (( -us “ ( R ‘ðī)) |s ( -us “ ( L ‘ðī))) = (( -us “ 𝑅) |s ( -us “ ðŋ)))
1356, 134eqtrd 2764 1 (𝜑 → ( -us ‘ðī) = (( -us “ 𝑅) |s ( -us “ ðŋ)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  âˆ€wral 3053  âˆƒwrex 3062  Vcvv 3466   ⊆ wss 3940  {csn 4620   class class class wbr 5138  ran crn 5667   “ cima 5669  Fun wfun 6527   Fn wfn 6528  â€“onto→wfo 6531  â€˜cfv 6533  (class class class)co 7401   No csur 27477   <s cslt 27478   â‰Īs csle 27581   <<s csslt 27617   |s cscut 27619   L cleft 27676   R cright 27677   -us cnegs 27836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-1o 8461  df-2o 8462  df-nadd 8660  df-no 27480  df-slt 27481  df-bday 27482  df-sle 27582  df-sslt 27618  df-scut 27620  df-0s 27661  df-made 27678  df-old 27679  df-left 27681  df-right 27682  df-norec 27759  df-norec2 27770  df-adds 27781  df-negs 27838
This theorem is referenced by:  renegscl  28097
  Copyright terms: Public domain W3C validator