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

Theorem dicfnN 37197
Description: Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dicfn.l = (le‘𝐾)
dicfn.a 𝐴 = (Atoms‘𝐾)
dicfn.h 𝐻 = (LHyp‘𝐾)
dicfn.i 𝐼 = ((DIsoC‘𝐾)‘𝑊)
Assertion
Ref Expression
dicfnN ((𝐾𝑉𝑊𝐻) → 𝐼 Fn {𝑝𝐴 ∣ ¬ 𝑝 𝑊})
Distinct variable groups:   ,𝑝   𝐴,𝑝   𝐾,𝑝   𝑊,𝑝
Allowed substitution hints:   𝐻(𝑝)   𝐼(𝑝)   𝑉(𝑝)

Proof of Theorem dicfnN
Dummy variables 𝑞 𝑓 𝑠 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 4845 . . . . . . 7 (𝑝 = 𝑞 → (𝑝 𝑊𝑞 𝑊))
21notbid 310 . . . . . 6 (𝑝 = 𝑞 → (¬ 𝑝 𝑊 ↔ ¬ 𝑞 𝑊))
32elrab 3555 . . . . 5 (𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} ↔ (𝑞𝐴 ∧ ¬ 𝑞 𝑊))
4 dicfn.l . . . . . . 7 = (le‘𝐾)
5 dicfn.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
6 dicfn.h . . . . . . 7 𝐻 = (LHyp‘𝐾)
7 eqid 2798 . . . . . . 7 ((oc‘𝐾)‘𝑊) = ((oc‘𝐾)‘𝑊)
8 eqid 2798 . . . . . . 7 ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
9 eqid 2798 . . . . . . 7 ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
10 dicfn.i . . . . . . 7 𝐼 = ((DIsoC‘𝐾)‘𝑊)
114, 5, 6, 7, 8, 9, 10dicval 37190 . . . . . 6 (((𝐾𝑉𝑊𝐻) ∧ (𝑞𝐴 ∧ ¬ 𝑞 𝑊)) → (𝐼𝑞) = {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))})
12 fvex 6423 . . . . . 6 (𝐼𝑞) ∈ V
1311, 12syl6eqelr 2886 . . . . 5 (((𝐾𝑉𝑊𝐻) ∧ (𝑞𝐴 ∧ ¬ 𝑞 𝑊)) → {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))} ∈ V)
143, 13sylan2b 588 . . . 4 (((𝐾𝑉𝑊𝐻) ∧ 𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊}) → {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))} ∈ V)
1514ralrimiva 3146 . . 3 ((𝐾𝑉𝑊𝐻) → ∀𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))} ∈ V)
16 eqid 2798 . . . 4 (𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))}) = (𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))})
1716fnmpt 6230 . . 3 (∀𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))} ∈ V → (𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))}) Fn {𝑝𝐴 ∣ ¬ 𝑝 𝑊})
1815, 17syl 17 . 2 ((𝐾𝑉𝑊𝐻) → (𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))}) Fn {𝑝𝐴 ∣ ¬ 𝑝 𝑊})
194, 5, 6, 7, 8, 9, 10dicfval 37189 . . 3 ((𝐾𝑉𝑊𝐻) → 𝐼 = (𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))}))
2019fneq1d 6191 . 2 ((𝐾𝑉𝑊𝐻) → (𝐼 Fn {𝑝𝐴 ∣ ¬ 𝑝 𝑊} ↔ (𝑞 ∈ {𝑝𝐴 ∣ ¬ 𝑝 𝑊} ↦ {⟨𝑓, 𝑠⟩ ∣ (𝑓 = (𝑠‘(𝑢 ∈ ((LTrn‘𝐾)‘𝑊)(𝑢‘((oc‘𝐾)‘𝑊)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))}) Fn {𝑝𝐴 ∣ ¬ 𝑝 𝑊}))
2118, 20mpbird 249 1 ((𝐾𝑉𝑊𝐻) → 𝐼 Fn {𝑝𝐴 ∣ ¬ 𝑝 𝑊})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385   = wceq 1653  wcel 2157  wral 3088  {crab 3092  Vcvv 3384   class class class wbr 4842  {copab 4904  cmpt 4921   Fn wfn 6095  cfv 6100  crio 6837  lecple 16271  occoc 16272  Atomscatm 35277  LHypclh 35998  LTrncltrn 36115  TEndoctendo 36766  DIsoCcdic 37186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-rep 4963  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4628  df-iun 4711  df-br 4843  df-opab 4905  df-mpt 4922  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-dic 37187
This theorem is referenced by:  dicdmN  37198
  Copyright terms: Public domain W3C validator