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 40018
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 2733 . . . 4 ((DIsoAβ€˜πΎ)β€˜π‘Š) = ((DIsoAβ€˜πΎ)β€˜π‘Š)
7 dibval3.i . . . 4 𝐼 = ((DIsoBβ€˜πΎ)β€˜π‘Š)
81, 2, 3, 4, 5, 6, 7dibval2 40015 . . 3 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (πΌβ€˜π‘‹) = ((((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) Γ— { 0 }))
98eleq2d 2820 . 2 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (π‘Œ ∈ (πΌβ€˜π‘‹) ↔ π‘Œ ∈ ((((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) Γ— { 0 })))
10 dibval3.r . . . . . . 7 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
111, 2, 3, 4, 10, 6diaelval 39904 . . . . . 6 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ↔ (𝑓 ∈ 𝑇 ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
1211anbi1d 631 . . . . 5 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ ((𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩) ↔ ((𝑓 ∈ 𝑇 ∧ (π‘…β€˜π‘“) ≀ 𝑋) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩)))
13 an13 646 . . . . . . . 8 ((π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ (𝑠 ∈ { 0 } ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)))
14 velsn 4645 . . . . . . . . 9 (𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
1514anbi1i 625 . . . . . . . 8 ((𝑠 ∈ { 0 } ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)) ↔ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)))
1613, 15bitri 275 . . . . . . 7 ((π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)))
1716exbii 1851 . . . . . 6 (βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ βˆƒπ‘ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)))
184fvexi 6906 . . . . . . . . 9 𝑇 ∈ V
1918mptex 7225 . . . . . . . 8 (𝑔 ∈ 𝑇 ↦ ( I β†Ύ 𝐡)) ∈ V
205, 19eqeltri 2830 . . . . . . 7 0 ∈ V
21 opeq2 4875 . . . . . . . . 9 (𝑠 = 0 β†’ βŸ¨π‘“, π‘ βŸ© = βŸ¨π‘“, 0 ⟩)
2221eqeq2d 2744 . . . . . . . 8 (𝑠 = 0 β†’ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ↔ π‘Œ = βŸ¨π‘“, 0 ⟩))
2322anbi2d 630 . . . . . . 7 (𝑠 = 0 β†’ ((𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©) ↔ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩)))
2420, 23ceqsexv 3526 . . . . . 6 (βˆƒπ‘ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, π‘ βŸ©)) ↔ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩))
2517, 24bitri 275 . . . . 5 (βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩))
26 anass 470 . . . . . 6 (((𝑓 ∈ 𝑇 ∧ π‘Œ = βŸ¨π‘“, 0 ⟩) ∧ (π‘…β€˜π‘“) ≀ 𝑋) ↔ (𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
27 an32 645 . . . . . 6 (((𝑓 ∈ 𝑇 ∧ π‘Œ = βŸ¨π‘“, 0 ⟩) ∧ (π‘…β€˜π‘“) ≀ 𝑋) ↔ ((𝑓 ∈ 𝑇 ∧ (π‘…β€˜π‘“) ≀ 𝑋) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩))
2826, 27bitr3i 277 . . . . 5 ((𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)) ↔ ((𝑓 ∈ 𝑇 ∧ (π‘…β€˜π‘“) ≀ 𝑋) ∧ π‘Œ = βŸ¨π‘“, 0 ⟩))
2912, 25, 283bitr4g 314 . . . 4 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ (𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋))))
3029exbidv 1925 . . 3 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (βˆƒπ‘“βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })) ↔ βˆƒπ‘“(𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋))))
31 elxp 5700 . . 3 (π‘Œ ∈ ((((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) Γ— { 0 }) ↔ βˆƒπ‘“βˆƒπ‘ (π‘Œ = βŸ¨π‘“, π‘ βŸ© ∧ (𝑓 ∈ (((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) ∧ 𝑠 ∈ { 0 })))
32 df-rex 3072 . . 3 (βˆƒπ‘“ ∈ 𝑇 (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋) ↔ βˆƒπ‘“(𝑓 ∈ 𝑇 ∧ (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
3330, 31, 323bitr4g 314 . 2 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (π‘Œ ∈ ((((DIsoAβ€˜πΎ)β€˜π‘Š)β€˜π‘‹) Γ— { 0 }) ↔ βˆƒπ‘“ ∈ 𝑇 (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
349, 33bitrd 279 1 (((𝐾 ∈ 𝑉 ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ 𝐡 ∧ 𝑋 ≀ π‘Š)) β†’ (π‘Œ ∈ (πΌβ€˜π‘‹) ↔ βˆƒπ‘“ ∈ 𝑇 (π‘Œ = βŸ¨π‘“, 0 ⟩ ∧ (π‘…β€˜π‘“) ≀ 𝑋)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆƒwrex 3071  Vcvv 3475  {csn 4629  βŸ¨cop 4635   class class class wbr 5149   ↦ cmpt 5232   I cid 5574   Γ— cxp 5675   β†Ύ cres 5679  β€˜cfv 6544  Basecbs 17144  lecple 17204  LHypclh 38855  LTrncltrn 38972  trLctrl 39029  DIsoAcdia 39899  DIsoBcdib 40009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-disoa 39900  df-dib 40010
This theorem is referenced by:  cdlemn11pre  40081  dihord2pre  40096
  Copyright terms: Public domain W3C validator