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

Theorem ressval3d 16619
 Description: Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 3-Jul-2022.)
Hypotheses
Ref Expression
ressval3d.r 𝑅 = (𝑆s 𝐴)
ressval3d.b 𝐵 = (Base‘𝑆)
ressval3d.e 𝐸 = (Base‘ndx)
ressval3d.s (𝜑𝑆𝑉)
ressval3d.f (𝜑 → Fun 𝑆)
ressval3d.d (𝜑𝐸 ∈ dom 𝑆)
ressval3d.u (𝜑𝐴𝐵)
Assertion
Ref Expression
ressval3d (𝜑𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))

Proof of Theorem ressval3d
StepHypRef Expression
1 ressval3d.u . 2 (𝜑𝐴𝐵)
2 sspss 4005 . . . 4 (𝐴𝐵 ↔ (𝐴𝐵𝐴 = 𝐵))
3 dfpss3 3992 . . . . 5 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
43orbi1i 911 . . . 4 ((𝐴𝐵𝐴 = 𝐵) ↔ ((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∨ 𝐴 = 𝐵))
52, 4bitri 278 . . 3 (𝐴𝐵 ↔ ((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∨ 𝐴 = 𝐵))
6 simplr 768 . . . . . . 7 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → ¬ 𝐵𝐴)
7 ressval3d.s . . . . . . . 8 (𝜑𝑆𝑉)
87adantl 485 . . . . . . 7 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → 𝑆𝑉)
9 simpl 486 . . . . . . . 8 ((𝐴𝐵 ∧ ¬ 𝐵𝐴) → 𝐴𝐵)
10 ressval3d.b . . . . . . . . . 10 𝐵 = (Base‘𝑆)
1110fvexi 6672 . . . . . . . . 9 𝐵 ∈ V
1211a1i 11 . . . . . . . 8 (𝜑𝐵 ∈ V)
13 ssexg 5193 . . . . . . . 8 ((𝐴𝐵𝐵 ∈ V) → 𝐴 ∈ V)
149, 12, 13syl2an 598 . . . . . . 7 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → 𝐴 ∈ V)
15 ressval3d.r . . . . . . . 8 𝑅 = (𝑆s 𝐴)
1615, 10ressval2 16611 . . . . . . 7 ((¬ 𝐵𝐴𝑆𝑉𝐴 ∈ V) → 𝑅 = (𝑆 sSet ⟨(Base‘ndx), (𝐴𝐵)⟩))
176, 8, 14, 16syl3anc 1368 . . . . . 6 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → 𝑅 = (𝑆 sSet ⟨(Base‘ndx), (𝐴𝐵)⟩))
18 ressval3d.e . . . . . . . . . 10 𝐸 = (Base‘ndx)
1918a1i 11 . . . . . . . . 9 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → 𝐸 = (Base‘ndx))
20 df-ss 3875 . . . . . . . . . . . . 13 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
2120biimpi 219 . . . . . . . . . . . 12 (𝐴𝐵 → (𝐴𝐵) = 𝐴)
2221eqcomd 2764 . . . . . . . . . . 11 (𝐴𝐵𝐴 = (𝐴𝐵))
2322adantr 484 . . . . . . . . . 10 ((𝐴𝐵 ∧ ¬ 𝐵𝐴) → 𝐴 = (𝐴𝐵))
2423adantr 484 . . . . . . . . 9 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → 𝐴 = (𝐴𝐵))
2519, 24opeq12d 4771 . . . . . . . 8 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → ⟨𝐸, 𝐴⟩ = ⟨(Base‘ndx), (𝐴𝐵)⟩)
2625eqcomd 2764 . . . . . . 7 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → ⟨(Base‘ndx), (𝐴𝐵)⟩ = ⟨𝐸, 𝐴⟩)
2726oveq2d 7166 . . . . . 6 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → (𝑆 sSet ⟨(Base‘ndx), (𝐴𝐵)⟩) = (𝑆 sSet ⟨𝐸, 𝐴⟩))
2817, 27eqtrd 2793 . . . . 5 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∧ 𝜑) → 𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
2928ex 416 . . . 4 ((𝐴𝐵 ∧ ¬ 𝐵𝐴) → (𝜑𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩)))
3015a1i 11 . . . . . . 7 ((𝐴 = 𝐵𝜑) → 𝑅 = (𝑆s 𝐴))
31 oveq2 7158 . . . . . . . 8 (𝐴 = 𝐵 → (𝑆s 𝐴) = (𝑆s 𝐵))
3231adantr 484 . . . . . . 7 ((𝐴 = 𝐵𝜑) → (𝑆s 𝐴) = (𝑆s 𝐵))
337adantl 485 . . . . . . . 8 ((𝐴 = 𝐵𝜑) → 𝑆𝑉)
3410ressid 16617 . . . . . . . 8 (𝑆𝑉 → (𝑆s 𝐵) = 𝑆)
3533, 34syl 17 . . . . . . 7 ((𝐴 = 𝐵𝜑) → (𝑆s 𝐵) = 𝑆)
3630, 32, 353eqtrd 2797 . . . . . 6 ((𝐴 = 𝐵𝜑) → 𝑅 = 𝑆)
37 df-base 16547 . . . . . . . 8 Base = Slot 1
38 1nn 11685 . . . . . . . 8 1 ∈ ℕ
39 ressval3d.f . . . . . . . 8 (𝜑 → Fun 𝑆)
40 ressval3d.d . . . . . . . . 9 (𝜑𝐸 ∈ dom 𝑆)
4118, 40eqeltrrid 2857 . . . . . . . 8 (𝜑 → (Base‘ndx) ∈ dom 𝑆)
4237, 38, 7, 39, 41setsidvald 16572 . . . . . . 7 (𝜑𝑆 = (𝑆 sSet ⟨(Base‘ndx), (Base‘𝑆)⟩))
4342adantl 485 . . . . . 6 ((𝐴 = 𝐵𝜑) → 𝑆 = (𝑆 sSet ⟨(Base‘ndx), (Base‘𝑆)⟩))
4418a1i 11 . . . . . . . . 9 ((𝐴 = 𝐵𝜑) → 𝐸 = (Base‘ndx))
45 simpl 486 . . . . . . . . . 10 ((𝐴 = 𝐵𝜑) → 𝐴 = 𝐵)
4645, 10eqtrdi 2809 . . . . . . . . 9 ((𝐴 = 𝐵𝜑) → 𝐴 = (Base‘𝑆))
4744, 46opeq12d 4771 . . . . . . . 8 ((𝐴 = 𝐵𝜑) → ⟨𝐸, 𝐴⟩ = ⟨(Base‘ndx), (Base‘𝑆)⟩)
4847eqcomd 2764 . . . . . . 7 ((𝐴 = 𝐵𝜑) → ⟨(Base‘ndx), (Base‘𝑆)⟩ = ⟨𝐸, 𝐴⟩)
4948oveq2d 7166 . . . . . 6 ((𝐴 = 𝐵𝜑) → (𝑆 sSet ⟨(Base‘ndx), (Base‘𝑆)⟩) = (𝑆 sSet ⟨𝐸, 𝐴⟩))
5036, 43, 493eqtrd 2797 . . . . 5 ((𝐴 = 𝐵𝜑) → 𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
5150ex 416 . . . 4 (𝐴 = 𝐵 → (𝜑𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩)))
5229, 51jaoi 854 . . 3 (((𝐴𝐵 ∧ ¬ 𝐵𝐴) ∨ 𝐴 = 𝐵) → (𝜑𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩)))
535, 52sylbi 220 . 2 (𝐴𝐵 → (𝜑𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩)))
541, 53mpcom 38 1 (𝜑𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  Vcvv 3409   ∩ cin 3857   ⊆ wss 3858   ⊊ wpss 3859  ⟨cop 4528  dom cdm 5524  Fun wfun 6329  ‘cfv 6335  (class class class)co 7150  1c1 10576  ndxcnx 16538   sSet csts 16539  Basecbs 16541   ↾s cress 16542 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-1cn 10633  ax-addcl 10635 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-nn 11675  df-ndx 16544  df-slot 16545  df-base 16547  df-sets 16548  df-ress 16549 This theorem is referenced by:  estrres  17455
 Copyright terms: Public domain W3C validator