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

Theorem pclfinN 39377
Description: The projective subspace closure of a set equals the union of the closures of its finite subsets. Analogous to Lemma 3.3.6 of [PtakPulmannova] p. 72. Compare the closed subspace version pclfinclN 39427. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
pclfin.a 𝐴 = (Atoms‘𝐾)
pclfin.c 𝑈 = (PCl‘𝐾)
Assertion
Ref Expression
pclfinN ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑈𝑋) = 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))
Distinct variable groups:   𝑦,𝐴   𝑦,𝑈   𝑦,𝐾   𝑦,𝑋

Proof of Theorem pclfinN
Dummy variables 𝑞 𝑝 𝑟 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 481 . . 3 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → 𝐾 ∈ AtLat)
2 elin 3963 . . . . . . . 8 (𝑦 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑦 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝑋))
3 elpwi 4611 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
43adantl 480 . . . . . . . 8 ((𝑦 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝑋) → 𝑦𝑋)
52, 4sylbi 216 . . . . . . 7 (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → 𝑦𝑋)
6 simpll 765 . . . . . . . . 9 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑦𝑋) → 𝐾 ∈ AtLat)
7 sstr 3988 . . . . . . . . . . . 12 ((𝑦𝑋𝑋𝐴) → 𝑦𝐴)
87ancoms 457 . . . . . . . . . . 11 ((𝑋𝐴𝑦𝑋) → 𝑦𝐴)
98adantll 712 . . . . . . . . . 10 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑦𝑋) → 𝑦𝐴)
10 pclfin.a . . . . . . . . . . 11 𝐴 = (Atoms‘𝐾)
11 eqid 2727 . . . . . . . . . . 11 (PSubSp‘𝐾) = (PSubSp‘𝐾)
12 pclfin.c . . . . . . . . . . 11 𝑈 = (PCl‘𝐾)
1310, 11, 12pclclN 39368 . . . . . . . . . 10 ((𝐾 ∈ AtLat ∧ 𝑦𝐴) → (𝑈𝑦) ∈ (PSubSp‘𝐾))
146, 9, 13syl2anc 582 . . . . . . . . 9 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑦𝑋) → (𝑈𝑦) ∈ (PSubSp‘𝐾))
1510, 11psubssat 39231 . . . . . . . . 9 ((𝐾 ∈ AtLat ∧ (𝑈𝑦) ∈ (PSubSp‘𝐾)) → (𝑈𝑦) ⊆ 𝐴)
166, 14, 15syl2anc 582 . . . . . . . 8 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑦𝑋) → (𝑈𝑦) ⊆ 𝐴)
1716ex 411 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑦𝑋 → (𝑈𝑦) ⊆ 𝐴))
185, 17syl5 34 . . . . . 6 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → (𝑈𝑦) ⊆ 𝐴))
1918ralrimiv 3141 . . . . 5 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → ∀𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ⊆ 𝐴)
20 iunss 5050 . . . . 5 ( 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ⊆ 𝐴)
2119, 20sylibr 233 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ⊆ 𝐴)
22 eliun 5002 . . . . . . . . 9 (𝑝 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈𝑦))
23 fveq2 6900 . . . . . . . . . . 11 (𝑦 = 𝑤 → (𝑈𝑦) = (𝑈𝑤))
2423eleq2d 2814 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑝 ∈ (𝑈𝑦) ↔ 𝑝 ∈ (𝑈𝑤)))
2524cbvrexvw 3231 . . . . . . . . 9 (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈𝑦) ↔ ∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈𝑤))
2622, 25bitri 274 . . . . . . . 8 (𝑝 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ↔ ∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈𝑤))
27 eliun 5002 . . . . . . . . 9 (𝑞 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑦))
28 fveq2 6900 . . . . . . . . . . 11 (𝑦 = 𝑣 → (𝑈𝑦) = (𝑈𝑣))
2928eleq2d 2814 . . . . . . . . . 10 (𝑦 = 𝑣 → (𝑞 ∈ (𝑈𝑦) ↔ 𝑞 ∈ (𝑈𝑣)))
3029cbvrexvw 3231 . . . . . . . . 9 (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑦) ↔ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑣))
3127, 30bitri 274 . . . . . . . 8 (𝑞 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ↔ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑣))
3226, 31anbi12i 626 . . . . . . 7 ((𝑝 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ∧ 𝑞 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)) ↔ (∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈𝑤) ∧ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑣)))
33 elin 3963 . . . . . . . . . . 11 (𝑤 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑤 ∈ Fin ∧ 𝑤 ∈ 𝒫 𝑋))
34 elpwi 4611 . . . . . . . . . . . 12 (𝑤 ∈ 𝒫 𝑋𝑤𝑋)
3534anim2i 615 . . . . . . . . . . 11 ((𝑤 ∈ Fin ∧ 𝑤 ∈ 𝒫 𝑋) → (𝑤 ∈ Fin ∧ 𝑤𝑋))
3633, 35sylbi 216 . . . . . . . . . 10 (𝑤 ∈ (Fin ∩ 𝒫 𝑋) → (𝑤 ∈ Fin ∧ 𝑤𝑋))
37 elin 3963 . . . . . . . . . . . . . 14 (𝑣 ∈ (Fin ∩ 𝒫 𝑋) ↔ (𝑣 ∈ Fin ∧ 𝑣 ∈ 𝒫 𝑋))
38 elpwi 4611 . . . . . . . . . . . . . . 15 (𝑣 ∈ 𝒫 𝑋𝑣𝑋)
3938anim2i 615 . . . . . . . . . . . . . 14 ((𝑣 ∈ Fin ∧ 𝑣 ∈ 𝒫 𝑋) → (𝑣 ∈ Fin ∧ 𝑣𝑋))
4037, 39sylbi 216 . . . . . . . . . . . . 13 (𝑣 ∈ (Fin ∩ 𝒫 𝑋) → (𝑣 ∈ Fin ∧ 𝑣𝑋))
41 simp2rl 1239 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ∈ Fin)
42 simp12l 1283 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ∈ Fin)
43 unfi 9201 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 ∈ Fin ∧ 𝑣 ∈ Fin) → (𝑤𝑣) ∈ Fin)
4441, 42, 43syl2anc 582 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤𝑣) ∈ Fin)
45 simp2rr 1240 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤𝑋)
46 simp12r 1284 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣𝑋)
4745, 46unssd 4186 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤𝑣) ⊆ 𝑋)
48 vex 3475 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 ∈ V
49 vex 3475 . . . . . . . . . . . . . . . . . . . . . 22 𝑣 ∈ V
5048, 49unex 7752 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑣) ∈ V
5150elpw 4608 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑣) ∈ 𝒫 𝑋 ↔ (𝑤𝑣) ⊆ 𝑋)
5247, 51sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤𝑣) ∈ 𝒫 𝑋)
5344, 52elind 4194 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤𝑣) ∈ (Fin ∩ 𝒫 𝑋))
54 simp11l 1281 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝐾 ∈ AtLat)
55 simp11r 1282 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑋𝐴)
5645, 55sstrd 3990 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤𝐴)
5746, 55sstrd 3990 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣𝐴)
5856, 57unssd 4186 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤𝑣) ⊆ 𝐴)
5910, 11, 12pclclN 39368 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ AtLat ∧ (𝑤𝑣) ⊆ 𝐴) → (𝑈‘(𝑤𝑣)) ∈ (PSubSp‘𝐾))
6054, 58, 59syl2anc 582 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘(𝑤𝑣)) ∈ (PSubSp‘𝐾))
61 simp3l 1198 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟𝐴)
62 ssun1 4172 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 ⊆ (𝑤𝑣)
6362a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ (𝑤𝑣))
6410, 12pclssN 39371 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ AtLat ∧ 𝑤 ⊆ (𝑤𝑣) ∧ (𝑤𝑣) ⊆ 𝐴) → (𝑈𝑤) ⊆ (𝑈‘(𝑤𝑣)))
6554, 63, 58, 64syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈𝑤) ⊆ (𝑈‘(𝑤𝑣)))
66 simp2l 1196 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑝 ∈ (𝑈𝑤))
6765, 66sseldd 3981 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑝 ∈ (𝑈‘(𝑤𝑣)))
68 ssun2 4173 . . . . . . . . . . . . . . . . . . . . . 22 𝑣 ⊆ (𝑤𝑣)
6968a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ (𝑤𝑣))
7010, 12pclssN 39371 . . . . . . . . . . . . . . . . . . . . 21 ((𝐾 ∈ AtLat ∧ 𝑣 ⊆ (𝑤𝑣) ∧ (𝑤𝑣) ⊆ 𝐴) → (𝑈𝑣) ⊆ (𝑈‘(𝑤𝑣)))
7154, 69, 58, 70syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈𝑣) ⊆ (𝑈‘(𝑤𝑣)))
72 simp13 1202 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑞 ∈ (𝑈𝑣))
7371, 72sseldd 3981 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑞 ∈ (𝑈‘(𝑤𝑣)))
74 simp3r 1199 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))
75 eqid 2727 . . . . . . . . . . . . . . . . . . . 20 (le‘𝐾) = (le‘𝐾)
76 eqid 2727 . . . . . . . . . . . . . . . . . . . 20 (join‘𝐾) = (join‘𝐾)
7775, 76, 10, 11psubspi2N 39225 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ AtLat ∧ (𝑈‘(𝑤𝑣)) ∈ (PSubSp‘𝐾) ∧ 𝑟𝐴) ∧ (𝑝 ∈ (𝑈‘(𝑤𝑣)) ∧ 𝑞 ∈ (𝑈‘(𝑤𝑣)) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ (𝑈‘(𝑤𝑣)))
7854, 60, 61, 67, 73, 74, 77syl33anc 1382 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ (𝑈‘(𝑤𝑣)))
79 fveq2 6900 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑤𝑣) → (𝑈𝑦) = (𝑈‘(𝑤𝑣)))
8079eleq2d 2814 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑤𝑣) → (𝑟 ∈ (𝑈𝑦) ↔ 𝑟 ∈ (𝑈‘(𝑤𝑣))))
8180rspcev 3609 . . . . . . . . . . . . . . . . . 18 (((𝑤𝑣) ∈ (Fin ∩ 𝒫 𝑋) ∧ 𝑟 ∈ (𝑈‘(𝑤𝑣))) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈𝑦))
8253, 78, 81syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈𝑦))
83 eliun 5002 . . . . . . . . . . . . . . . . 17 (𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈𝑦))
8482, 83sylibr 233 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) ∧ (𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) ∧ (𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))
85843exp 1116 . . . . . . . . . . . . . . 15 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) → ((𝑝 ∈ (𝑈𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤𝑋)) → ((𝑟𝐴𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))))
8685exp5c 443 . . . . . . . . . . . . . 14 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣𝑋) ∧ 𝑞 ∈ (𝑈𝑣)) → (𝑝 ∈ (𝑈𝑤) → ((𝑤 ∈ Fin ∧ 𝑤𝑋) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))))))
87863exp 1116 . . . . . . . . . . . . 13 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → ((𝑣 ∈ Fin ∧ 𝑣𝑋) → (𝑞 ∈ (𝑈𝑣) → (𝑝 ∈ (𝑈𝑤) → ((𝑤 ∈ Fin ∧ 𝑤𝑋) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))))))))
8840, 87syl5 34 . . . . . . . . . . . 12 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑣 ∈ (Fin ∩ 𝒫 𝑋) → (𝑞 ∈ (𝑈𝑣) → (𝑝 ∈ (𝑈𝑤) → ((𝑤 ∈ Fin ∧ 𝑤𝑋) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))))))))
8988rexlimdv 3149 . . . . . . . . . . 11 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑣) → (𝑝 ∈ (𝑈𝑤) → ((𝑤 ∈ Fin ∧ 𝑤𝑋) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))))))
9089com24 95 . . . . . . . . . 10 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → ((𝑤 ∈ Fin ∧ 𝑤𝑋) → (𝑝 ∈ (𝑈𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑣) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))))))
9136, 90syl5 34 . . . . . . . . 9 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑤 ∈ (Fin ∩ 𝒫 𝑋) → (𝑝 ∈ (𝑈𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑣) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))))))
9291rexlimdv 3149 . . . . . . . 8 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑣) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))))))
9392impd 409 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → ((∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈𝑤) ∧ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈𝑣)) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))))
9432, 93biimtrid 241 . . . . . 6 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → ((𝑝 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ∧ 𝑞 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)) → (𝑟𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))))
9594ralrimdv 3148 . . . . 5 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → ((𝑝 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ∧ 𝑞 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)) → ∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))))
9695ralrimivv 3194 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → ∀𝑝 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)∀𝑞 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))
9775, 76, 10, 11ispsubsp 39222 . . . . 5 (𝐾 ∈ AtLat → ( 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ∈ (PSubSp‘𝐾) ↔ ( 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ⊆ 𝐴 ∧ ∀𝑝 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)∀𝑞 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))))
9897adantr 479 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → ( 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ∈ (PSubSp‘𝐾) ↔ ( 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ⊆ 𝐴 ∧ ∀𝑝 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)∀𝑞 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)∀𝑟𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))))
9921, 96, 98mpbir2and 711 . . 3 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ∈ (PSubSp‘𝐾))
100 snfi 9073 . . . . . . . . 9 {𝑤} ∈ Fin
101100a1i 11 . . . . . . . 8 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → {𝑤} ∈ Fin)
102 snelpwi 5447 . . . . . . . . 9 (𝑤𝑋 → {𝑤} ∈ 𝒫 𝑋)
103102adantl 480 . . . . . . . 8 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → {𝑤} ∈ 𝒫 𝑋)
104101, 103elind 4194 . . . . . . 7 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → {𝑤} ∈ (Fin ∩ 𝒫 𝑋))
105 vsnid 4668 . . . . . . . 8 𝑤 ∈ {𝑤}
106 simpll 765 . . . . . . . . 9 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → 𝐾 ∈ AtLat)
107 ssel2 3975 . . . . . . . . . . 11 ((𝑋𝐴𝑤𝑋) → 𝑤𝐴)
108107adantll 712 . . . . . . . . . 10 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → 𝑤𝐴)
10910, 11snatpsubN 39227 . . . . . . . . . 10 ((𝐾 ∈ AtLat ∧ 𝑤𝐴) → {𝑤} ∈ (PSubSp‘𝐾))
110106, 108, 109syl2anc 582 . . . . . . . . 9 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → {𝑤} ∈ (PSubSp‘𝐾))
11111, 12pclidN 39373 . . . . . . . . 9 ((𝐾 ∈ AtLat ∧ {𝑤} ∈ (PSubSp‘𝐾)) → (𝑈‘{𝑤}) = {𝑤})
112106, 110, 111syl2anc 582 . . . . . . . 8 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → (𝑈‘{𝑤}) = {𝑤})
113105, 112eleqtrrid 2835 . . . . . . 7 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → 𝑤 ∈ (𝑈‘{𝑤}))
114 fveq2 6900 . . . . . . . . 9 (𝑦 = {𝑤} → (𝑈𝑦) = (𝑈‘{𝑤}))
115114eleq2d 2814 . . . . . . . 8 (𝑦 = {𝑤} → (𝑤 ∈ (𝑈𝑦) ↔ 𝑤 ∈ (𝑈‘{𝑤})))
116115rspcev 3609 . . . . . . 7 (({𝑤} ∈ (Fin ∩ 𝒫 𝑋) ∧ 𝑤 ∈ (𝑈‘{𝑤})) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈𝑦))
117104, 113, 116syl2anc 582 . . . . . 6 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑤𝑋) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈𝑦))
118117ex 411 . . . . 5 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑤𝑋 → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈𝑦)))
119 eliun 5002 . . . . 5 (𝑤 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈𝑦))
120118, 119imbitrrdi 251 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑤𝑋𝑤 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦)))
121120ssrdv 3986 . . 3 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → 𝑋 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))
122 simpr 483 . . . . . . . . . 10 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑦𝑋) → 𝑦𝑋)
123 simplr 767 . . . . . . . . . 10 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑦𝑋) → 𝑋𝐴)
12410, 12pclssN 39371 . . . . . . . . . 10 ((𝐾 ∈ AtLat ∧ 𝑦𝑋𝑋𝐴) → (𝑈𝑦) ⊆ (𝑈𝑋))
1256, 122, 123, 124syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑦𝑋) → (𝑈𝑦) ⊆ (𝑈𝑋))
126125sseld 3979 . . . . . . . 8 (((𝐾 ∈ AtLat ∧ 𝑋𝐴) ∧ 𝑦𝑋) → (𝑤 ∈ (𝑈𝑦) → 𝑤 ∈ (𝑈𝑋)))
127126ex 411 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑦𝑋 → (𝑤 ∈ (𝑈𝑦) → 𝑤 ∈ (𝑈𝑋))))
1285, 127syl5 34 . . . . . 6 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → (𝑤 ∈ (𝑈𝑦) → 𝑤 ∈ (𝑈𝑋))))
129128rexlimdv 3149 . . . . 5 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈𝑦) → 𝑤 ∈ (𝑈𝑋)))
130119, 129biimtrid 241 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑤 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) → 𝑤 ∈ (𝑈𝑋)))
131130ssrdv 3986 . . 3 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ⊆ (𝑈𝑋))
13211, 12pclbtwnN 39374 . . 3 (((𝐾 ∈ AtLat ∧ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ∈ (PSubSp‘𝐾)) ∧ (𝑋 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ∧ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) ⊆ (𝑈𝑋))) → 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) = (𝑈𝑋))
1331, 99, 121, 131, 132syl22anc 837 . 2 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦) = (𝑈𝑋))
134133eqcomd 2733 1 ((𝐾 ∈ AtLat ∧ 𝑋𝐴) → (𝑈𝑋) = 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3057  wrex 3066  cun 3945  cin 3946  wss 3947  𝒫 cpw 4604  {csn 4630   ciun 4998   class class class wbr 5150  cfv 6551  (class class class)co 7424  Fincfn 8968  lecple 17245  joincjn 18308  Atomscatm 38739  AtLatcal 38740  PSubSpcpsubsp 38973  PClcpclN 39364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-riota 7380  df-ov 7427  df-oprab 7428  df-om 7875  df-1o 8491  df-en 8969  df-fin 8972  df-proset 18292  df-poset 18310  df-plt 18327  df-lub 18343  df-glb 18344  df-join 18345  df-meet 18346  df-p0 18422  df-lat 18429  df-covers 38742  df-ats 38743  df-atl 38774  df-psubsp 38980  df-pclN 39365
This theorem is referenced by:  pclcmpatN  39378
  Copyright terms: Public domain W3C validator