Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dibvalrel Structured version   Visualization version   GIF version

Theorem dibvalrel 35953
Description: The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014.)
Hypotheses
Ref Expression
dibcl.h 𝐻 = (LHyp‘𝐾)
dibcl.i 𝐼 = ((DIsoB‘𝐾)‘𝑊)
Assertion
Ref Expression
dibvalrel ((𝐾𝑉𝑊𝐻) → Rel (𝐼𝑋))

Proof of Theorem dibvalrel
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 relxp 5190 . . 3 Rel ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))})
2 dibcl.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
3 eqid 2621 . . . . . . . 8 ((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊)
4 dibcl.i . . . . . . . 8 𝐼 = ((DIsoB‘𝐾)‘𝑊)
52, 3, 4dibdiadm 35945 . . . . . . 7 ((𝐾𝑉𝑊𝐻) → dom 𝐼 = dom ((DIsoA‘𝐾)‘𝑊))
65eleq2d 2684 . . . . . 6 ((𝐾𝑉𝑊𝐻) → (𝑋 ∈ dom 𝐼𝑋 ∈ dom ((DIsoA‘𝐾)‘𝑊)))
76biimpa 501 . . . . 5 (((𝐾𝑉𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ dom ((DIsoA‘𝐾)‘𝑊))
8 eqid 2621 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
9 eqid 2621 . . . . . 6 ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
10 eqid 2621 . . . . . 6 ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾))) = ( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))
118, 2, 9, 10, 3, 4dibval 35932 . . . . 5 (((𝐾𝑉𝑊𝐻) ∧ 𝑋 ∈ dom ((DIsoA‘𝐾)‘𝑊)) → (𝐼𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))}))
127, 11syldan 487 . . . 4 (((𝐾𝑉𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))}))
1312releqd 5166 . . 3 (((𝐾𝑉𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → (Rel (𝐼𝑋) ↔ Rel ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × {( ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ (Base‘𝐾)))})))
141, 13mpbiri 248 . 2 (((𝐾𝑉𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → Rel (𝐼𝑋))
15 rel0 5206 . . . 4 Rel ∅
16 ndmfv 6177 . . . . 5 𝑋 ∈ dom 𝐼 → (𝐼𝑋) = ∅)
1716releqd 5166 . . . 4 𝑋 ∈ dom 𝐼 → (Rel (𝐼𝑋) ↔ Rel ∅))
1815, 17mpbiri 248 . . 3 𝑋 ∈ dom 𝐼 → Rel (𝐼𝑋))
1918adantl 482 . 2 (((𝐾𝑉𝑊𝐻) ∧ ¬ 𝑋 ∈ dom 𝐼) → Rel (𝐼𝑋))
2014, 19pm2.61dan 831 1 ((𝐾𝑉𝑊𝐻) → Rel (𝐼𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1480  wcel 1987  c0 3893  {csn 4150  cmpt 4675   I cid 4986   × cxp 5074  dom cdm 5076  cres 5078  Rel wrel 5081  cfv 5849  Basecbs 15784  LHypclh 34771  LTrncltrn 34888  DIsoAcdia 35818  DIsoBcdib 35928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-dib 35929
This theorem is referenced by:  dibglbN  35956  dib2dim  36033  dih2dimbALTN  36035
  Copyright terms: Public domain W3C validator