| Step | Hyp | Ref
| Expression |
| 1 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
| 2 | 1 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐾 ∈ HL ∧ 𝑥 ⊆ 𝐴) ↔ (𝐾 ∈ HL ∧ ∅ ⊆ 𝐴))) |
| 3 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑈‘𝑥) = (𝑈‘∅)) |
| 4 | 3 | eleq1d 2826 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝑈‘𝑥) ∈ 𝑆 ↔ (𝑈‘∅) ∈ 𝑆)) |
| 5 | 2, 4 | imbi12d 344 |
. . . 4
⊢ (𝑥 = ∅ → (((𝐾 ∈ HL ∧ 𝑥 ⊆ 𝐴) → (𝑈‘𝑥) ∈ 𝑆) ↔ ((𝐾 ∈ HL ∧ ∅ ⊆ 𝐴) → (𝑈‘∅) ∈ 𝑆))) |
| 6 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴)) |
| 7 | 6 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐾 ∈ HL ∧ 𝑥 ⊆ 𝐴) ↔ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴))) |
| 8 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑈‘𝑥) = (𝑈‘𝑦)) |
| 9 | 8 | eleq1d 2826 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑈‘𝑥) ∈ 𝑆 ↔ (𝑈‘𝑦) ∈ 𝑆)) |
| 10 | 7, 9 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝐾 ∈ HL ∧ 𝑥 ⊆ 𝐴) → (𝑈‘𝑥) ∈ 𝑆) ↔ ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → (𝑈‘𝑦) ∈ 𝑆))) |
| 11 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) |
| 12 | 11 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐾 ∈ HL ∧ 𝑥 ⊆ 𝐴) ↔ (𝐾 ∈ HL ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴))) |
| 13 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑈‘𝑥) = (𝑈‘(𝑦 ∪ {𝑧}))) |
| 14 | 13 | eleq1d 2826 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑈‘𝑥) ∈ 𝑆 ↔ (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆)) |
| 15 | 12, 14 | imbi12d 344 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((𝐾 ∈ HL ∧ 𝑥 ⊆ 𝐴) → (𝑈‘𝑥) ∈ 𝑆) ↔ ((𝐾 ∈ HL ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆))) |
| 16 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 ⊆ 𝐴 ↔ 𝑋 ⊆ 𝐴)) |
| 17 | 16 | anbi2d 630 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝐾 ∈ HL ∧ 𝑥 ⊆ 𝐴) ↔ (𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴))) |
| 18 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑈‘𝑥) = (𝑈‘𝑋)) |
| 19 | 18 | eleq1d 2826 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝑈‘𝑥) ∈ 𝑆 ↔ (𝑈‘𝑋) ∈ 𝑆)) |
| 20 | 17, 19 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝑋 → (((𝐾 ∈ HL ∧ 𝑥 ⊆ 𝐴) → (𝑈‘𝑥) ∈ 𝑆) ↔ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ∈ 𝑆))) |
| 21 | | pclfincl.c |
. . . . . . 7
⊢ 𝑈 = (PCl‘𝐾) |
| 22 | 21 | pcl0N 39924 |
. . . . . 6
⊢ (𝐾 ∈ HL → (𝑈‘∅) =
∅) |
| 23 | | pclfincl.s |
. . . . . . 7
⊢ 𝑆 = (PSubCl‘𝐾) |
| 24 | 23 | 0psubclN 39945 |
. . . . . 6
⊢ (𝐾 ∈ HL → ∅ ∈
𝑆) |
| 25 | 22, 24 | eqeltrd 2841 |
. . . . 5
⊢ (𝐾 ∈ HL → (𝑈‘∅) ∈ 𝑆) |
| 26 | 25 | adantr 480 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ∅ ⊆
𝐴) → (𝑈‘∅) ∈ 𝑆) |
| 27 | | anass 468 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) ∧ 𝑧 ∈ 𝐴) ↔ (𝐾 ∈ HL ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
| 28 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
| 29 | 28 | snss 4785 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴) |
| 30 | 29 | anbi2i 623 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐴) ↔ (𝑦 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴)) |
| 31 | | unss 4190 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
| 32 | 30, 31 | bitri 275 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐴) ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
| 33 | 32 | anbi2i 623 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ (𝐾 ∈ HL ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) |
| 34 | 27, 33 | bitr2i 276 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) ↔ ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) ∧ 𝑧 ∈ 𝐴)) |
| 35 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝑦 = ∅) |
| 36 | 35 | uneq1d 4167 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑦 ∪ {𝑧}) = (∅ ∪ {𝑧})) |
| 37 | | uncom 4158 |
. . . . . . . . . . . . . . 15
⊢ (∅
∪ {𝑧}) = ({𝑧} ∪
∅) |
| 38 | | un0 4394 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ∪ ∅) = {𝑧} |
| 39 | 37, 38 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (∅
∪ {𝑧}) = {𝑧} |
| 40 | 36, 39 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑦 ∪ {𝑧}) = {𝑧}) |
| 41 | 40 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘(𝑦 ∪ {𝑧})) = (𝑈‘{𝑧})) |
| 42 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝐾 ∈ HL) |
| 43 | | hlatl 39361 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
| 44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝐾 ∈ AtLat) |
| 45 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴) |
| 46 | | pclfincl.a |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = (Atoms‘𝐾) |
| 47 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(PSubSp‘𝐾) =
(PSubSp‘𝐾) |
| 48 | 46, 47 | snatpsubN 39752 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ AtLat ∧ 𝑧 ∈ 𝐴) → {𝑧} ∈ (PSubSp‘𝐾)) |
| 49 | 44, 45, 48 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → {𝑧} ∈ (PSubSp‘𝐾)) |
| 50 | 47, 21 | pclidN 39898 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ {𝑧} ∈ (PSubSp‘𝐾)) → (𝑈‘{𝑧}) = {𝑧}) |
| 51 | 42, 49, 50 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘{𝑧}) = {𝑧}) |
| 52 | 41, 51 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘(𝑦 ∪ {𝑧})) = {𝑧}) |
| 53 | 46, 23 | atpsubclN 39947 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑧 ∈ 𝐴) → {𝑧} ∈ 𝑆) |
| 54 | 42, 45, 53 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → {𝑧} ∈ 𝑆) |
| 55 | 52, 54 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 = ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆) |
| 56 | 55 | exp43 436 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ 𝑦 = ∅) → ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → ((𝑈‘𝑦) ∈ 𝑆 → (𝑧 ∈ 𝐴 → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆)))) |
| 57 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝐾 ∈ HL) |
| 58 | 46, 21 | pclssidN 39897 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ (𝑈‘𝑦)) |
| 59 | 58 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝑦 ⊆ (𝑈‘𝑦)) |
| 60 | | unss1 4185 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ (𝑈‘𝑦) → (𝑦 ∪ {𝑧}) ⊆ ((𝑈‘𝑦) ∪ {𝑧})) |
| 61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ ((𝑈‘𝑦) ∪ {𝑧})) |
| 62 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘𝑦) ∈ 𝑆) |
| 63 | 46, 23 | psubclssatN 39943 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ HL ∧ (𝑈‘𝑦) ∈ 𝑆) → (𝑈‘𝑦) ⊆ 𝐴) |
| 64 | 57, 62, 63 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘𝑦) ⊆ 𝐴) |
| 65 | | snssi 4808 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ 𝐴 → {𝑧} ⊆ 𝐴) |
| 66 | 65 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → {𝑧} ⊆ 𝐴) |
| 67 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(+𝑃‘𝐾) = (+𝑃‘𝐾) |
| 68 | 46, 67 | paddunssN 39810 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ HL ∧ (𝑈‘𝑦) ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) → ((𝑈‘𝑦) ∪ {𝑧}) ⊆ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) |
| 69 | 57, 64, 66, 68 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → ((𝑈‘𝑦) ∪ {𝑧}) ⊆ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) |
| 70 | 61, 69 | sstrd 3994 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) |
| 71 | 46, 67 | paddssat 39816 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ HL ∧ (𝑈‘𝑦) ⊆ 𝐴 ∧ {𝑧} ⊆ 𝐴) → ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ⊆ 𝐴) |
| 72 | 57, 64, 66, 71 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ⊆ 𝐴) |
| 73 | 46, 21 | pclssN 39896 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ HL ∧ (𝑦 ∪ {𝑧}) ⊆ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ∧ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ⊆ 𝐴) → (𝑈‘(𝑦 ∪ {𝑧})) ⊆ (𝑈‘((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}))) |
| 74 | 57, 70, 72, 73 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘(𝑦 ∪ {𝑧})) ⊆ (𝑈‘((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}))) |
| 75 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝑧 ∈ 𝐴) |
| 76 | 46, 67, 23 | paddatclN 39951 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ HL ∧ (𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) → ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ∈ 𝑆) |
| 77 | 57, 62, 75, 76 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ∈ 𝑆) |
| 78 | 47, 23 | psubclsubN 39942 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ HL ∧ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ∈ 𝑆) → ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ∈ (PSubSp‘𝐾)) |
| 79 | 57, 77, 78 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ∈ (PSubSp‘𝐾)) |
| 80 | 47, 21 | pclidN 39898 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ HL ∧ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ∈ (PSubSp‘𝐾)) → (𝑈‘((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) = ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) |
| 81 | 57, 79, 80 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) = ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) |
| 82 | 74, 81 | sseqtrd 4020 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘(𝑦 ∪ {𝑧})) ⊆ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) |
| 83 | 57 | hllatd 39365 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝐾 ∈ Lat) |
| 84 | | simpllr 776 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝑦 ≠ ∅) |
| 85 | 46, 21 | pcl0bN 39925 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → ((𝑈‘𝑦) = ∅ ↔ 𝑦 = ∅)) |
| 86 | 85 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → ((𝑈‘𝑦) = ∅ ↔ 𝑦 = ∅)) |
| 87 | 86 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → ((𝑈‘𝑦) ≠ ∅ ↔ 𝑦 ≠ ∅)) |
| 88 | 84, 87 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘𝑦) ≠ ∅) |
| 89 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(le‘𝐾) =
(le‘𝐾) |
| 90 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(join‘𝐾) =
(join‘𝐾) |
| 91 | 89, 90, 46, 67 | elpaddat 39806 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ Lat ∧ (𝑈‘𝑦) ⊆ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑈‘𝑦) ≠ ∅) → (𝑞 ∈ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ↔ (𝑞 ∈ 𝐴 ∧ ∃𝑝 ∈ (𝑈‘𝑦)𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)))) |
| 92 | 83, 64, 75, 88, 91 | syl31anc 1375 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑞 ∈ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ↔ (𝑞 ∈ 𝐴 ∧ ∃𝑝 ∈ (𝑈‘𝑦)𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)))) |
| 93 | | simp1rl 1239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → 𝐾 ∈ HL) |
| 94 | 93 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) → 𝐾 ∈ HL) |
| 95 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝐾 ∈ HL) |
| 96 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝑤 ∈ (PSubSp‘𝐾)) |
| 97 | | simpl13 1251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝑞 ∈ 𝐴) |
| 98 | | unss 4190 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ⊆ 𝑤 ∧ {𝑧} ⊆ 𝑤) ↔ (𝑦 ∪ {𝑧}) ⊆ 𝑤) |
| 99 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ⊆ 𝑤 ∧ {𝑧} ⊆ 𝑤) → 𝑦 ⊆ 𝑤) |
| 100 | 98, 99 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑦 ⊆ 𝑤) |
| 101 | 100 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝑦 ⊆ 𝑤) |
| 102 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝑝 ∈ (𝑈‘𝑦)) |
| 103 | 47, 21 | elpcliN 39895 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝑤 ∧ 𝑤 ∈ (PSubSp‘𝐾)) ∧ 𝑝 ∈ (𝑈‘𝑦)) → 𝑝 ∈ 𝑤) |
| 104 | 95, 101, 96, 102, 103 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝑝 ∈ 𝑤) |
| 105 | 28 | snss 4785 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ 𝑤 ↔ {𝑧} ⊆ 𝑤) |
| 106 | 105 | biimpri 228 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ({𝑧} ⊆ 𝑤 → 𝑧 ∈ 𝑤) |
| 107 | 106 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ⊆ 𝑤 ∧ {𝑧} ⊆ 𝑤) → 𝑧 ∈ 𝑤) |
| 108 | 98, 107 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑧 ∈ 𝑤) |
| 109 | 108 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝑧 ∈ 𝑤) |
| 110 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) |
| 111 | 89, 90, 46, 47 | psubspi2N 39750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾 ∈ HL ∧ 𝑤 ∈ (PSubSp‘𝐾) ∧ 𝑞 ∈ 𝐴) ∧ (𝑝 ∈ 𝑤 ∧ 𝑧 ∈ 𝑤 ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧))) → 𝑞 ∈ 𝑤) |
| 112 | 95, 96, 97, 104, 109, 110, 111 | syl33anc 1387 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑦 ∈ Fin
∧ 𝑦 ≠ ∅) ∧
(𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) ∧ 𝑝 ∈ (𝑈‘𝑦) ∧ 𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) ∧ (𝑤 ∈ (PSubSp‘𝐾) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝑤)) → 𝑞 ∈ 𝑤) |
| 113 | 112 | exp520 1358 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → (𝑝 ∈ (𝑈‘𝑦) → (𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧) → (𝑤 ∈ (PSubSp‘𝐾) → ((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑞 ∈ 𝑤))))) |
| 114 | 113 | rexlimdv 3153 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴) → (∃𝑝 ∈ (𝑈‘𝑦)𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧) → (𝑤 ∈ (PSubSp‘𝐾) → ((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑞 ∈ 𝑤)))) |
| 115 | 114 | 3expia 1122 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑞 ∈ 𝐴 → (∃𝑝 ∈ (𝑈‘𝑦)𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧) → (𝑤 ∈ (PSubSp‘𝐾) → ((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑞 ∈ 𝑤))))) |
| 116 | 115 | impd 410 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → ((𝑞 ∈ 𝐴 ∧ ∃𝑝 ∈ (𝑈‘𝑦)𝑞(le‘𝐾)(𝑝(join‘𝐾)𝑧)) → (𝑤 ∈ (PSubSp‘𝐾) → ((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑞 ∈ 𝑤)))) |
| 117 | 92, 116 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑞 ∈ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) → (𝑤 ∈ (PSubSp‘𝐾) → ((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑞 ∈ 𝑤)))) |
| 118 | 117 | ralrimdv 3152 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑞 ∈ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) → ∀𝑤 ∈ (PSubSp‘𝐾)((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑞 ∈ 𝑤))) |
| 119 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → 𝑦 ⊆ 𝐴) |
| 120 | 119, 75 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ 𝐴)) |
| 121 | 120, 32 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴) |
| 122 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑞 ∈ V |
| 123 | 46, 47, 21, 122 | elpclN 39894 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ HL ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (𝑞 ∈ (𝑈‘(𝑦 ∪ {𝑧})) ↔ ∀𝑤 ∈ (PSubSp‘𝐾)((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑞 ∈ 𝑤))) |
| 124 | 57, 121, 123 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑞 ∈ (𝑈‘(𝑦 ∪ {𝑧})) ↔ ∀𝑤 ∈ (PSubSp‘𝐾)((𝑦 ∪ {𝑧}) ⊆ 𝑤 → 𝑞 ∈ 𝑤))) |
| 125 | 118, 124 | sylibrd 259 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑞 ∈ ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) → 𝑞 ∈ (𝑈‘(𝑦 ∪ {𝑧})))) |
| 126 | 125 | ssrdv 3989 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧}) ⊆ (𝑈‘(𝑦 ∪ {𝑧}))) |
| 127 | 82, 126 | eqssd 4001 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘(𝑦 ∪ {𝑧})) = ((𝑈‘𝑦)(+𝑃‘𝐾){𝑧})) |
| 128 | 127, 77 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) ∧ (𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴)) ∧ ((𝑈‘𝑦) ∈ 𝑆 ∧ 𝑧 ∈ 𝐴)) → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆) |
| 129 | 128 | exp43 436 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ≠ ∅) → ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → ((𝑈‘𝑦) ∈ 𝑆 → (𝑧 ∈ 𝐴 → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆)))) |
| 130 | 56, 129 | pm2.61dane 3029 |
. . . . . . . 8
⊢ (𝑦 ∈ Fin → ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → ((𝑈‘𝑦) ∈ 𝑆 → (𝑧 ∈ 𝐴 → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆)))) |
| 131 | 130 | a2d 29 |
. . . . . . 7
⊢ (𝑦 ∈ Fin → (((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → (𝑈‘𝑦) ∈ 𝑆) → ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → (𝑧 ∈ 𝐴 → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆)))) |
| 132 | 131 | imp4b 421 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → (𝑈‘𝑦) ∈ 𝑆)) → (((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆)) |
| 133 | 34, 132 | biimtrid 242 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → (𝑈‘𝑦) ∈ 𝑆)) → ((𝐾 ∈ HL ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆)) |
| 134 | 133 | ex 412 |
. . . 4
⊢ (𝑦 ∈ Fin → (((𝐾 ∈ HL ∧ 𝑦 ⊆ 𝐴) → (𝑈‘𝑦) ∈ 𝑆) → ((𝐾 ∈ HL ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (𝑈‘(𝑦 ∪ {𝑧})) ∈ 𝑆))) |
| 135 | 5, 10, 15, 20, 26, 134 | findcard2 9204 |
. . 3
⊢ (𝑋 ∈ Fin → ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ∈ 𝑆)) |
| 136 | 135 | 3impib 1117 |
. 2
⊢ ((𝑋 ∈ Fin ∧ 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ∈ 𝑆) |
| 137 | 136 | 3coml 1128 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝑈‘𝑋) ∈ 𝑆) |