| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . 3
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → 𝐾 ∈ AtLat) |
| 2 | | elin 3967 |
. . . . . . . 8
⊢ (𝑦 ∈ (Fin ∩ 𝒫
𝑋) ↔ (𝑦 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝑋)) |
| 3 | | elpwi 4607 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) |
| 4 | 3 | adantl 481 |
. . . . . . . 8
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝑋) → 𝑦 ⊆ 𝑋) |
| 5 | 2, 4 | sylbi 217 |
. . . . . . 7
⊢ (𝑦 ∈ (Fin ∩ 𝒫
𝑋) → 𝑦 ⊆ 𝑋) |
| 6 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝐾 ∈ AtLat) |
| 7 | | sstr 3992 |
. . . . . . . . . . . 12
⊢ ((𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝐴) → 𝑦 ⊆ 𝐴) |
| 8 | 7 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝐴) |
| 9 | 8 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝐴) |
| 10 | | pclfin.a |
. . . . . . . . . . 11
⊢ 𝐴 = (Atoms‘𝐾) |
| 11 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(PSubSp‘𝐾) =
(PSubSp‘𝐾) |
| 12 | | pclfin.c |
. . . . . . . . . . 11
⊢ 𝑈 = (PCl‘𝐾) |
| 13 | 10, 11, 12 | pclclN 39893 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ AtLat ∧ 𝑦 ⊆ 𝐴) → (𝑈‘𝑦) ∈ (PSubSp‘𝐾)) |
| 14 | 6, 9, 13 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ∈ (PSubSp‘𝐾)) |
| 15 | 10, 11 | psubssat 39756 |
. . . . . . . . 9
⊢ ((𝐾 ∈ AtLat ∧ (𝑈‘𝑦) ∈ (PSubSp‘𝐾)) → (𝑈‘𝑦) ⊆ 𝐴) |
| 16 | 6, 14, 15 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ⊆ 𝐴) |
| 17 | 16 | ex 412 |
. . . . . . 7
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ⊆ 𝑋 → (𝑈‘𝑦) ⊆ 𝐴)) |
| 18 | 5, 17 | syl5 34 |
. . . . . 6
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → (𝑈‘𝑦) ⊆ 𝐴)) |
| 19 | 18 | ralrimiv 3145 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∀𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴) |
| 20 | | iunss 5045 |
. . . . 5
⊢ (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴) |
| 21 | 19, 20 | sylibr 234 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴) |
| 22 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑦)) |
| 23 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (𝑈‘𝑦) = (𝑈‘𝑤)) |
| 24 | 23 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝑝 ∈ (𝑈‘𝑦) ↔ 𝑝 ∈ (𝑈‘𝑤))) |
| 25 | 24 | cbvrexvw 3238 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
(Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑦) ↔ ∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤)) |
| 26 | 22, 25 | bitri 275 |
. . . . . . . 8
⊢ (𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤)) |
| 27 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑦)) |
| 28 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑣 → (𝑈‘𝑦) = (𝑈‘𝑣)) |
| 29 | 28 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → (𝑞 ∈ (𝑈‘𝑦) ↔ 𝑞 ∈ (𝑈‘𝑣))) |
| 30 | 29 | cbvrexvw 3238 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
(Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑦) ↔ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣)) |
| 31 | 27, 30 | bitri 275 |
. . . . . . . 8
⊢ (𝑞 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣)) |
| 32 | 26, 31 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑝 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)) ↔ (∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) ∧ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣))) |
| 33 | | elin 3967 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ (Fin ∩ 𝒫
𝑋) ↔ (𝑤 ∈ Fin ∧ 𝑤 ∈ 𝒫 𝑋)) |
| 34 | | elpwi 4607 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝒫 𝑋 → 𝑤 ⊆ 𝑋) |
| 35 | 34 | anim2i 617 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ Fin ∧ 𝑤 ∈ 𝒫 𝑋) → (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) |
| 36 | 33, 35 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑤 ∈ (Fin ∩ 𝒫
𝑋) → (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) |
| 37 | | elin 3967 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (Fin ∩ 𝒫
𝑋) ↔ (𝑣 ∈ Fin ∧ 𝑣 ∈ 𝒫 𝑋)) |
| 38 | | elpwi 4607 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝒫 𝑋 → 𝑣 ⊆ 𝑋) |
| 39 | 38 | anim2i 617 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ Fin ∧ 𝑣 ∈ 𝒫 𝑋) → (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋)) |
| 40 | 37, 39 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (Fin ∩ 𝒫
𝑋) → (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋)) |
| 41 | | simp2rl 1243 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ∈ Fin) |
| 42 | | simp12l 1287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ∈ Fin) |
| 43 | | unfi 9211 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ Fin ∧ 𝑣 ∈ Fin) → (𝑤 ∪ 𝑣) ∈ Fin) |
| 44 | 41, 42, 43 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ Fin) |
| 45 | | simp2rr 1244 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ 𝑋) |
| 46 | | simp12r 1288 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ 𝑋) |
| 47 | 45, 46 | unssd 4192 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ⊆ 𝑋) |
| 48 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑤 ∈ V |
| 49 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑣 ∈ V |
| 50 | 48, 49 | unex 7764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∪ 𝑣) ∈ V |
| 51 | 50 | elpw 4604 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∪ 𝑣) ∈ 𝒫 𝑋 ↔ (𝑤 ∪ 𝑣) ⊆ 𝑋) |
| 52 | 47, 51 | sylibr 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ 𝒫 𝑋) |
| 53 | 44, 52 | elind 4200 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ∈ (Fin ∩ 𝒫 𝑋)) |
| 54 | | simp11l 1285 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝐾 ∈ AtLat) |
| 55 | | simp11r 1286 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑋 ⊆ 𝐴) |
| 56 | 45, 55 | sstrd 3994 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ 𝐴) |
| 57 | 46, 55 | sstrd 3994 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ 𝐴) |
| 58 | 56, 57 | unssd 4192 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑤 ∪ 𝑣) ⊆ 𝐴) |
| 59 | 10, 11, 12 | pclclN 39893 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ AtLat ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾)) |
| 60 | 54, 58, 59 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾)) |
| 61 | | simp3l 1202 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ 𝐴) |
| 62 | | ssun1 4178 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑤 ⊆ (𝑤 ∪ 𝑣) |
| 63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑤 ⊆ (𝑤 ∪ 𝑣)) |
| 64 | 10, 12 | pclssN 39896 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ AtLat ∧ 𝑤 ⊆ (𝑤 ∪ 𝑣) ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘𝑤) ⊆ (𝑈‘(𝑤 ∪ 𝑣))) |
| 65 | 54, 63, 58, 64 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘𝑤) ⊆ (𝑈‘(𝑤 ∪ 𝑣))) |
| 66 | | simp2l 1200 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑝 ∈ (𝑈‘𝑤)) |
| 67 | 65, 66 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑝 ∈ (𝑈‘(𝑤 ∪ 𝑣))) |
| 68 | | ssun2 4179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑣 ⊆ (𝑤 ∪ 𝑣) |
| 69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑣 ⊆ (𝑤 ∪ 𝑣)) |
| 70 | 10, 12 | pclssN 39896 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ AtLat ∧ 𝑣 ⊆ (𝑤 ∪ 𝑣) ∧ (𝑤 ∪ 𝑣) ⊆ 𝐴) → (𝑈‘𝑣) ⊆ (𝑈‘(𝑤 ∪ 𝑣))) |
| 71 | 54, 69, 58, 70 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → (𝑈‘𝑣) ⊆ (𝑈‘(𝑤 ∪ 𝑣))) |
| 72 | | simp13 1206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑞 ∈ (𝑈‘𝑣)) |
| 73 | 71, 72 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑞 ∈ (𝑈‘(𝑤 ∪ 𝑣))) |
| 74 | | simp3r 1203 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) |
| 75 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(le‘𝐾) =
(le‘𝐾) |
| 76 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(join‘𝐾) =
(join‘𝐾) |
| 77 | 75, 76, 10, 11 | psubspi2N 39750 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 ∈ AtLat ∧ (𝑈‘(𝑤 ∪ 𝑣)) ∈ (PSubSp‘𝐾) ∧ 𝑟 ∈ 𝐴) ∧ (𝑝 ∈ (𝑈‘(𝑤 ∪ 𝑣)) ∧ 𝑞 ∈ (𝑈‘(𝑤 ∪ 𝑣)) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣))) |
| 78 | 54, 60, 61, 67, 73, 74, 77 | syl33anc 1387 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣))) |
| 79 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑤 ∪ 𝑣) → (𝑈‘𝑦) = (𝑈‘(𝑤 ∪ 𝑣))) |
| 80 | 79 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑤 ∪ 𝑣) → (𝑟 ∈ (𝑈‘𝑦) ↔ 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣)))) |
| 81 | 80 | rspcev 3622 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∪ 𝑣) ∈ (Fin ∩ 𝒫 𝑋) ∧ 𝑟 ∈ (𝑈‘(𝑤 ∪ 𝑣))) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦)) |
| 82 | 53, 78, 81 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦)) |
| 83 | | eliun 4995 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑟 ∈ (𝑈‘𝑦)) |
| 84 | 82, 83 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) ∧ (𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)) |
| 85 | 84 | 3exp 1120 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) → ((𝑝 ∈ (𝑈‘𝑤) ∧ (𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋)) → ((𝑟 ∈ 𝐴 ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)))) |
| 86 | 85 | exp5c 444 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ (𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) ∧ 𝑞 ∈ (𝑈‘𝑣)) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)))))) |
| 87 | 86 | 3exp 1120 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑣 ∈ Fin ∧ 𝑣 ⊆ 𝑋) → (𝑞 ∈ (𝑈‘𝑣) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)))))))) |
| 88 | 40, 87 | syl5 34 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑣 ∈ (Fin ∩ 𝒫 𝑋) → (𝑞 ∈ (𝑈‘𝑣) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)))))))) |
| 89 | 88 | rexlimdv 3153 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑝 ∈ (𝑈‘𝑤) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))))))) |
| 90 | 89 | com24 95 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝑋) → (𝑝 ∈ (𝑈‘𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))))))) |
| 91 | 36, 90 | syl5 34 |
. . . . . . . . 9
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ (Fin ∩ 𝒫 𝑋) → (𝑝 ∈ (𝑈‘𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))))))) |
| 92 | 91 | rexlimdv 3153 |
. . . . . . . 8
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) → (∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)))))) |
| 93 | 92 | impd 410 |
. . . . . . 7
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((∃𝑤 ∈ (Fin ∩ 𝒫 𝑋)𝑝 ∈ (𝑈‘𝑤) ∧ ∃𝑣 ∈ (Fin ∩ 𝒫 𝑋)𝑞 ∈ (𝑈‘𝑣)) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))))) |
| 94 | 32, 93 | biimtrid 242 |
. . . . . 6
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑝 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))))) |
| 95 | 94 | ralrimdv 3152 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ((𝑝 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) ∧ 𝑞 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)) → ∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)))) |
| 96 | 95 | ralrimivv 3200 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∀𝑝 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)∀𝑞 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))) |
| 97 | 75, 76, 10, 11 | ispsubsp 39747 |
. . . . 5
⊢ (𝐾 ∈ AtLat → (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾) ↔ (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴 ∧ ∀𝑝 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)∀𝑞 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))))) |
| 98 | 97 | adantr 480 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾) ↔ (∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ⊆ 𝐴 ∧ ∀𝑝 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)∀𝑞 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))))) |
| 99 | 21, 96, 98 | mpbir2and 713 |
. . 3
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾)) |
| 100 | | snfi 9083 |
. . . . . . . . 9
⊢ {𝑤} ∈ Fin |
| 101 | 100 | a1i 11 |
. . . . . . . 8
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ Fin) |
| 102 | | snelpwi 5448 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑋 → {𝑤} ∈ 𝒫 𝑋) |
| 103 | 102 | adantl 481 |
. . . . . . . 8
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ 𝒫 𝑋) |
| 104 | 101, 103 | elind 4200 |
. . . . . . 7
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ (Fin ∩ 𝒫 𝑋)) |
| 105 | | vsnid 4663 |
. . . . . . . 8
⊢ 𝑤 ∈ {𝑤} |
| 106 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝐾 ∈ AtLat) |
| 107 | | ssel2 3978 |
. . . . . . . . . . 11
⊢ ((𝑋 ⊆ 𝐴 ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝐴) |
| 108 | 107 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ 𝐴) |
| 109 | 10, 11 | snatpsubN 39752 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ AtLat ∧ 𝑤 ∈ 𝐴) → {𝑤} ∈ (PSubSp‘𝐾)) |
| 110 | 106, 108,
109 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → {𝑤} ∈ (PSubSp‘𝐾)) |
| 111 | 11, 12 | pclidN 39898 |
. . . . . . . . 9
⊢ ((𝐾 ∈ AtLat ∧ {𝑤} ∈ (PSubSp‘𝐾)) → (𝑈‘{𝑤}) = {𝑤}) |
| 112 | 106, 110,
111 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → (𝑈‘{𝑤}) = {𝑤}) |
| 113 | 105, 112 | eleqtrrid 2848 |
. . . . . . 7
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → 𝑤 ∈ (𝑈‘{𝑤})) |
| 114 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = {𝑤} → (𝑈‘𝑦) = (𝑈‘{𝑤})) |
| 115 | 114 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑦 = {𝑤} → (𝑤 ∈ (𝑈‘𝑦) ↔ 𝑤 ∈ (𝑈‘{𝑤}))) |
| 116 | 115 | rspcev 3622 |
. . . . . . 7
⊢ (({𝑤} ∈ (Fin ∩ 𝒫
𝑋) ∧ 𝑤 ∈ (𝑈‘{𝑤})) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦)) |
| 117 | 104, 113,
116 | syl2anc 584 |
. . . . . 6
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑤 ∈ 𝑋) → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦)) |
| 118 | 117 | ex 412 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ 𝑋 → ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦))) |
| 119 | | eliun 4995 |
. . . . 5
⊢ (𝑤 ∈ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ↔ ∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦)) |
| 120 | 118, 119 | imbitrrdi 252 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ 𝑋 → 𝑤 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦))) |
| 121 | 120 | ssrdv 3989 |
. . 3
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)) |
| 122 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑦 ⊆ 𝑋) |
| 123 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → 𝑋 ⊆ 𝐴) |
| 124 | 10, 12 | pclssN 39896 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ AtLat ∧ 𝑦 ⊆ 𝑋 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑦) ⊆ (𝑈‘𝑋)) |
| 125 | 6, 122, 123, 124 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑈‘𝑦) ⊆ (𝑈‘𝑋)) |
| 126 | 125 | sseld 3982 |
. . . . . . . 8
⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) ∧ 𝑦 ⊆ 𝑋) → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋))) |
| 127 | 126 | ex 412 |
. . . . . . 7
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ⊆ 𝑋 → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋)))) |
| 128 | 5, 127 | syl5 34 |
. . . . . 6
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑦 ∈ (Fin ∩ 𝒫 𝑋) → (𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋)))) |
| 129 | 128 | rexlimdv 3153 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (∃𝑦 ∈ (Fin ∩ 𝒫 𝑋)𝑤 ∈ (𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋))) |
| 130 | 119, 129 | biimtrid 242 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑤 ∈ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) → 𝑤 ∈ (𝑈‘𝑋))) |
| 131 | 130 | ssrdv 3989 |
. . 3
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) ⊆ (𝑈‘𝑋)) |
| 132 | 11, 12 | pclbtwnN 39899 |
. . 3
⊢ (((𝐾 ∈ AtLat ∧ ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) ∈ (PSubSp‘𝐾)) ∧ (𝑋 ⊆ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) ∧ ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) ⊆ (𝑈‘𝑋))) → ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦) = (𝑈‘𝑋)) |
| 133 | 1, 99, 121, 131, 132 | syl22anc 839 |
. 2
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦) = (𝑈‘𝑋)) |
| 134 | 133 | eqcomd 2743 |
1
⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪
𝑦 ∈ (Fin ∩
𝒫 𝑋)(𝑈‘𝑦)) |