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

Theorem dibelval3 40104
Description: Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014.)
Hypotheses
Ref Expression
dibval3.b 𝐡 = (Baseβ€˜πΎ)
dibval3.l ≀ = (leβ€˜πΎ)
dibval3.h 𝐻 = (LHypβ€˜πΎ)
dibval3.t 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
dibval3.r 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
dibval3.o 0 = (𝑔 ∈ 𝑇 ↦ ( I β†Ύ 𝐡))
dibval3.i 𝐼 = ((DIsoBβ€˜πΎ)β€˜π‘Š)
Assertion
Ref Expression
dibelval3 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (π‘Œ ∈ (πΌβ€˜π‘‹) ↔ βˆƒπ‘“ ∈ 𝑇 (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
Distinct variable groups:   𝑓,𝐾   𝑔,𝐾   𝑇,𝑓   𝑓,π‘Š   𝑔,π‘Š   𝑓,𝑋   ≀ ,𝑓   𝐡,𝑓   𝑓,𝐻   0 ,𝑓   𝑇,𝑔   𝑓,𝑉   𝑓,π‘Œ
Allowed substitution hints:   𝐡(𝑔)   𝑅(𝑓,𝑔)   𝐻(𝑔)   𝐼(𝑓,𝑔)   ≀ (𝑔)   𝑉(𝑔)   𝑋(𝑔)   π‘Œ(𝑔)   0 (𝑔)

Proof of Theorem dibelval3
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 dibval3.b . . . 4 𝐡 = (Baseβ€˜πΎ)
2 dibval3.l . . . 4 ≀ = (leβ€˜πΎ)
3 dibval3.h . . . 4 𝐻 = (LHypβ€˜πΎ)
4 dibval3.t . . . 4 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
5 dibval3.o . . . 4 0 = (𝑔 ∈ 𝑇 ↦ ( I β†Ύ 𝐡))
6 eqid 2732 . . . 4 ((DIsoAβ€˜πΎ)β€˜π‘Š) = ((DIsoAβ€˜πΎ)β€˜π‘Š)
7 dibval3.i . . . 4 𝐼 = ((DIsoBβ€˜πΎ)β€˜π‘Š)
81, 2, 3, 4, 5, 6, 7dibval2 40101 . . 3 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (πΌβ€˜π‘‹) = ((((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) Γ— { 0 }))
98eleq2d 2819 . 2 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (π‘Œ ∈ (πΌβ€˜π‘‹) ↔ π‘Œ ∈ ((((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) Γ— { 0 })))
10 dibval3.r . . . . . . 7 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
111, 2, 3, 4, 10, 6diaelval 39990 . . . . . 6 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ↔ (𝑓 ∈ 𝑇 ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
1211anbi1d 630 . . . . 5 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ ((𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩) ↔ ((𝑓 ∈ 𝑇 ∧ (π‘…β€˜π‘“) ≀ 𝑋) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩)))
13 an13 645 . . . . . . . 8 ((π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ (𝑠 ∈ { 0 } ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)))
14 velsn 4644 . . . . . . . . 9 (𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
1514anbi1i 624 . . . . . . . 8 ((𝑠 ∈ { 0 } ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)) ↔ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)))
1613, 15bitri 274 . . . . . . 7 ((π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)))
1716exbii 1850 . . . . . 6 (βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ βˆƒπ‘ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)))
184fvexi 6905 . . . . . . . . 9 𝑇 ∈ V
1918mptex 7227 . . . . . . . 8 (𝑔 ∈ 𝑇 ↦ ( I β†Ύ 𝐡)) ∈ V
205, 19eqeltri 2829 . . . . . . 7 0 ∈ V
21 opeq2 4874 . . . . . . . . 9 (𝑠 = 0 β†’ βŸ¨π‘“, π‘ βŸ© = βŸ¨π‘“, 0 ⟩)
2221eqeq2d 2743 . . . . . . . 8 (𝑠 = 0 β†’ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ↔ π‘Œ = βŸ¨π‘“, 0 ⟩))
2322anbi2d 629 . . . . . . 7 (𝑠 = 0 β†’ ((𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©) ↔ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩)))
2420, 23ceqsexv 3525 . . . . . 6 (βˆƒπ‘ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)) ↔ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩))
2517, 24bitri 274 . . . . 5 (βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩))
26 anass 469 . . . . . 6 (((𝑓 ∈ 𝑇 ∧ π‘Œ = βŸ¨π‘“, 0 ⟩) ∧ (π‘…β€˜π‘“) ≀ 𝑋) ↔ (𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
27 an32 644 . . . . . 6 (((𝑓 ∈ 𝑇 ∧ π‘Œ = βŸ¨π‘“, 0 ⟩) ∧ (π‘…β€˜π‘“) ≀ 𝑋) ↔ ((𝑓 ∈ 𝑇 ∧ (π‘…β€˜π‘“) ≀ 𝑋) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩))
2826, 27bitr3i 276 . . . . 5 ((𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)) ↔ ((𝑓 ∈ 𝑇 ∧ (π‘…β€˜π‘“) ≀ 𝑋) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩))
2912, 25, 283bitr4g 313 . . . 4 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ (𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋))))
3029exbidv 1924 . . 3 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (βˆƒπ‘“βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ βˆƒπ‘“(𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋))))
31 elxp 5699 . . 3 (π‘Œ ∈ ((((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) Γ— { 0 }) ↔ βˆƒπ‘“βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })))
32 df-rex 3071 . . 3 (βˆƒπ‘“ ∈ 𝑇 (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋) ↔ βˆƒπ‘“(𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
3330, 31, 323bitr4g 313 . 2 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (π‘Œ ∈ ((((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) Γ— { 0 }) ↔ βˆƒπ‘“ ∈ 𝑇 (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
349, 33bitrd 278 1 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (π‘Œ ∈ (πΌβ€˜π‘‹) ↔ βˆƒπ‘“ ∈ 𝑇 (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  βˆƒwrex 3070  Vcvv 3474  {csn 4628  βŸ¨cop 4634   class class class wbr 5148   ↦ cmpt 5231   I cid 5573   Γ— cxp 5674   β†Ύ cres 5678  β€˜cfv 6543  Basecbs 17146  lecple 17206  LHypclh 38941  LTrncltrn 39058  trLctrl 39115  DIsoAcdia 39985  DIsoBcdib 40095
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-disoa 39986  df-dib 40096
This theorem is referenced by:  cdlemn11pre  40167  dihord2pre  40182
  Copyright terms: Public domain W3C validator