![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ressid2 | Structured version Visualization version GIF version |
Description: General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
Ref | Expression |
---|---|
ressbas.r | ⊢ 𝑅 = (𝑊 ↾s 𝐴) |
ressbas.b | ⊢ 𝐵 = (Base‘𝑊) |
Ref | Expression |
---|---|
ressid2 | ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressbas.r | . . . 4 ⊢ 𝑅 = (𝑊 ↾s 𝐴) | |
2 | ressbas.b | . . . 4 ⊢ 𝐵 = (Base‘𝑊) | |
3 | 1, 2 | ressval 17285 | . . 3 ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) |
4 | iftrue 4554 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) = 𝑊) | |
5 | 3, 4 | sylan9eqr 2796 | . 2 ⊢ ((𝐵 ⊆ 𝐴 ∧ (𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌)) → 𝑅 = 𝑊) |
6 | 5 | 3impb 1115 | 1 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2103 ∩ cin 3969 ⊆ wss 3970 ifcif 4548 〈cop 4654 ‘cfv 6572 (class class class)co 7445 sSet csts 17205 ndxcnx 17235 Basecbs 17253 ↾s cress 17282 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-sep 5320 ax-nul 5327 ax-pr 5450 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3439 df-v 3484 df-sbc 3799 df-dif 3973 df-un 3975 df-in 3977 df-ss 3987 df-nul 4348 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5170 df-opab 5232 df-id 5597 df-xp 5705 df-rel 5706 df-cnv 5707 df-co 5708 df-dm 5709 df-iota 6524 df-fun 6574 df-fv 6580 df-ov 7448 df-oprab 7449 df-mpo 7450 df-ress 17283 |
This theorem is referenced by: ressbas 17288 ressbasOLD 17289 resseqnbas 17295 resslemOLD 17296 ress0 17297 ressid 17298 ressinbas 17299 ressress 17302 rescabs 17891 rescabsOLD 17892 0symgefmndeq 19430 snsymgefmndeq 19431 mgpress 20171 mgpressOLD 20172 psgnghm2 21617 evl1maprhm 22397 resvsca 33313 extdg1id 33668 |
Copyright terms: Public domain | W3C validator |