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

Theorem pclclN 36907
Description: Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
pclfval.a 𝐴 = (Atoms‘𝐾)
pclfval.s 𝑆 = (PSubSp‘𝐾)
pclfval.c 𝑈 = (PCl‘𝐾)
Assertion
Ref Expression
pclclN ((𝐾𝑉𝑋𝐴) → (𝑈𝑋) ∈ 𝑆)

Proof of Theorem pclclN
Dummy variables 𝑦 𝑞 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pclfval.a . . 3 𝐴 = (Atoms‘𝐾)
2 pclfval.s . . 3 𝑆 = (PSubSp‘𝐾)
3 pclfval.c . . 3 𝑈 = (PCl‘𝐾)
41, 2, 3pclvalN 36906 . 2 ((𝐾𝑉𝑋𝐴) → (𝑈𝑋) = {𝑦𝑆𝑋𝑦})
51, 2atpsubN 36769 . . . 4 (𝐾𝑉𝐴𝑆)
6 sseq2 3990 . . . . 5 (𝑦 = 𝐴 → (𝑋𝑦𝑋𝐴))
76intminss 4893 . . . 4 ((𝐴𝑆𝑋𝐴) → {𝑦𝑆𝑋𝑦} ⊆ 𝐴)
85, 7sylan 580 . . 3 ((𝐾𝑉𝑋𝐴) → {𝑦𝑆𝑋𝑦} ⊆ 𝐴)
9 r19.26 3167 . . . . . . . 8 (∀𝑦𝑆 ((𝑋𝑦𝑝𝑦) ∧ (𝑋𝑦𝑞𝑦)) ↔ (∀𝑦𝑆 (𝑋𝑦𝑝𝑦) ∧ ∀𝑦𝑆 (𝑋𝑦𝑞𝑦)))
10 jcab 518 . . . . . . . . 9 ((𝑋𝑦 → (𝑝𝑦𝑞𝑦)) ↔ ((𝑋𝑦𝑝𝑦) ∧ (𝑋𝑦𝑞𝑦)))
1110ralbii 3162 . . . . . . . 8 (∀𝑦𝑆 (𝑋𝑦 → (𝑝𝑦𝑞𝑦)) ↔ ∀𝑦𝑆 ((𝑋𝑦𝑝𝑦) ∧ (𝑋𝑦𝑞𝑦)))
12 vex 3495 . . . . . . . . . 10 𝑝 ∈ V
1312elintrab 4879 . . . . . . . . 9 (𝑝 {𝑦𝑆𝑋𝑦} ↔ ∀𝑦𝑆 (𝑋𝑦𝑝𝑦))
14 vex 3495 . . . . . . . . . 10 𝑞 ∈ V
1514elintrab 4879 . . . . . . . . 9 (𝑞 {𝑦𝑆𝑋𝑦} ↔ ∀𝑦𝑆 (𝑋𝑦𝑞𝑦))
1613, 15anbi12i 626 . . . . . . . 8 ((𝑝 {𝑦𝑆𝑋𝑦} ∧ 𝑞 {𝑦𝑆𝑋𝑦}) ↔ (∀𝑦𝑆 (𝑋𝑦𝑝𝑦) ∧ ∀𝑦𝑆 (𝑋𝑦𝑞𝑦)))
179, 11, 163bitr4ri 305 . . . . . . 7 ((𝑝 {𝑦𝑆𝑋𝑦} ∧ 𝑞 {𝑦𝑆𝑋𝑦}) ↔ ∀𝑦𝑆 (𝑋𝑦 → (𝑝𝑦𝑞𝑦)))
18 simpll1 1204 . . . . . . . . . . . . . 14 ((((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) ∧ (𝑝𝑦𝑞𝑦)) → 𝐾𝑉)
19 simplr 765 . . . . . . . . . . . . . 14 ((((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) ∧ (𝑝𝑦𝑞𝑦)) → 𝑦𝑆)
20 simpll3 1206 . . . . . . . . . . . . . 14 ((((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) ∧ (𝑝𝑦𝑞𝑦)) → 𝑟𝐴)
21 simprl 767 . . . . . . . . . . . . . 14 ((((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) ∧ (𝑝𝑦𝑞𝑦)) → 𝑝𝑦)
22 simprr 769 . . . . . . . . . . . . . 14 ((((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) ∧ (𝑝𝑦𝑞𝑦)) → 𝑞𝑦)
23 simpll2 1205 . . . . . . . . . . . . . 14 ((((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) ∧ (𝑝𝑦𝑞𝑦)) → 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))
24 eqid 2818 . . . . . . . . . . . . . . 15 (le‘𝐾) = (le‘𝐾)
25 eqid 2818 . . . . . . . . . . . . . . 15 (join‘𝐾) = (join‘𝐾)
2624, 25, 1, 2psubspi2N 36764 . . . . . . . . . . . . . 14 (((𝐾𝑉𝑦𝑆𝑟𝐴) ∧ (𝑝𝑦𝑞𝑦𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟𝑦)
2718, 19, 20, 21, 22, 23, 26syl33anc 1377 . . . . . . . . . . . . 13 ((((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) ∧ (𝑝𝑦𝑞𝑦)) → 𝑟𝑦)
2827ex 413 . . . . . . . . . . . 12 (((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) → ((𝑝𝑦𝑞𝑦) → 𝑟𝑦))
2928imim2d 57 . . . . . . . . . . 11 (((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) ∧ 𝑦𝑆) → ((𝑋𝑦 → (𝑝𝑦𝑞𝑦)) → (𝑋𝑦𝑟𝑦)))
3029ralimdva 3174 . . . . . . . . . 10 ((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) → (∀𝑦𝑆 (𝑋𝑦 → (𝑝𝑦𝑞𝑦)) → ∀𝑦𝑆 (𝑋𝑦𝑟𝑦)))
31 vex 3495 . . . . . . . . . . 11 𝑟 ∈ V
3231elintrab 4879 . . . . . . . . . 10 (𝑟 {𝑦𝑆𝑋𝑦} ↔ ∀𝑦𝑆 (𝑋𝑦𝑟𝑦))
3330, 32syl6ibr 253 . . . . . . . . 9 ((𝐾𝑉𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ∧ 𝑟𝐴) → (∀𝑦𝑆 (𝑋𝑦 → (𝑝𝑦𝑞𝑦)) → 𝑟 {𝑦𝑆𝑋𝑦}))
34333exp 1111 . . . . . . . 8 (𝐾𝑉 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → (𝑟𝐴 → (∀𝑦𝑆 (𝑋𝑦 → (𝑝𝑦𝑞𝑦)) → 𝑟 {𝑦𝑆𝑋𝑦}))))
3534com24 95 . . . . . . 7 (𝐾𝑉 → (∀𝑦𝑆 (𝑋𝑦 → (𝑝𝑦𝑞𝑦)) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 {𝑦𝑆𝑋𝑦}))))
3617, 35syl5bi 243 . . . . . 6 (𝐾𝑉 → ((𝑝 {𝑦𝑆𝑋𝑦} ∧ 𝑞 {𝑦𝑆𝑋𝑦}) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 {𝑦𝑆𝑋𝑦}))))
3736ralrimdv 3185 . . . . 5 (𝐾𝑉 → ((𝑝 {𝑦𝑆𝑋𝑦} ∧ 𝑞 {𝑦𝑆𝑋𝑦}) → ∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 {𝑦𝑆𝑋𝑦})))
3837ralrimivv 3187 . . . 4 (𝐾𝑉 → ∀𝑝 {𝑦𝑆𝑋𝑦}∀𝑞 {𝑦𝑆𝑋𝑦}∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 {𝑦𝑆𝑋𝑦}))
3938adantr 481 . . 3 ((𝐾𝑉𝑋𝐴) → ∀𝑝 {𝑦𝑆𝑋𝑦}∀𝑞 {𝑦𝑆𝑋𝑦}∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 {𝑦𝑆𝑋𝑦}))
4024, 25, 1, 2ispsubsp 36761 . . . 4 (𝐾𝑉 → ( {𝑦𝑆𝑋𝑦} ∈ 𝑆 ↔ ( {𝑦𝑆𝑋𝑦} ⊆ 𝐴 ∧ ∀𝑝 {𝑦𝑆𝑋𝑦}∀𝑞 {𝑦𝑆𝑋𝑦}∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 {𝑦𝑆𝑋𝑦}))))
4140adantr 481 . . 3 ((𝐾𝑉𝑋𝐴) → ( {𝑦𝑆𝑋𝑦} ∈ 𝑆 ↔ ( {𝑦𝑆𝑋𝑦} ⊆ 𝐴 ∧ ∀𝑝 {𝑦𝑆𝑋𝑦}∀𝑞 {𝑦𝑆𝑋𝑦}∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 {𝑦𝑆𝑋𝑦}))))
428, 39, 41mpbir2and 709 . 2 ((𝐾𝑉𝑋𝐴) → {𝑦𝑆𝑋𝑦} ∈ 𝑆)
434, 42eqeltrd 2910 1 ((𝐾𝑉𝑋𝐴) → (𝑈𝑋) ∈ 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wral 3135  {crab 3139  wss 3933   cint 4867   class class class wbr 5057  cfv 6348  (class class class)co 7145  lecple 16560  joincjn 17542  Atomscatm 36279  PSubSpcpsubsp 36512  PClcpclN 36903
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-psubsp 36519  df-pclN 36904
This theorem is referenced by:  pclunN  36914  pclfinN  36916
  Copyright terms: Public domain W3C validator