| Step | Hyp | Ref
| Expression |
| 1 | | ssel 3977 |
. . . . . . 7
⊢ (𝑋 ⊆ 𝑌 → (𝑝 ∈ 𝑋 → 𝑝 ∈ 𝑌)) |
| 2 | 1 | orim1d 968 |
. . . . . 6
⊢ (𝑋 ⊆ 𝑌 → ((𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍) → (𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍))) |
| 3 | | ssrexv 4053 |
. . . . . . 7
⊢ (𝑋 ⊆ 𝑌 → (∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟) → ∃𝑞 ∈ 𝑌 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))) |
| 4 | 3 | anim2d 612 |
. . . . . 6
⊢ (𝑋 ⊆ 𝑌 → ((𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)) → (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑌 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)))) |
| 5 | 2, 4 | orim12d 967 |
. . . . 5
⊢ (𝑋 ⊆ 𝑌 → (((𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍) ∨ (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))) → ((𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍) ∨ (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑌 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))))) |
| 6 | 5 | adantl 481 |
. . . 4
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ 𝑋 ⊆ 𝑌) → (((𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍) ∨ (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))) → ((𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍) ∨ (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑌 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))))) |
| 7 | | simpl1 1192 |
. . . . 5
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ 𝑋 ⊆ 𝑌) → 𝐾 ∈ 𝐵) |
| 8 | | sstr 3992 |
. . . . . . 7
⊢ ((𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ 𝐴) |
| 9 | 8 | 3ad2antr2 1190 |
. . . . . 6
⊢ ((𝑋 ⊆ 𝑌 ∧ (𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → 𝑋 ⊆ 𝐴) |
| 10 | 9 | ancoms 458 |
. . . . 5
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ 𝑋 ⊆ 𝑌) → 𝑋 ⊆ 𝐴) |
| 11 | | simpl3 1194 |
. . . . 5
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ 𝑋 ⊆ 𝑌) → 𝑍 ⊆ 𝐴) |
| 12 | | eqid 2737 |
. . . . . 6
⊢
(le‘𝐾) =
(le‘𝐾) |
| 13 | | eqid 2737 |
. . . . . 6
⊢
(join‘𝐾) =
(join‘𝐾) |
| 14 | | padd0.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
| 15 | | padd0.p |
. . . . . 6
⊢ + =
(+𝑃‘𝐾) |
| 16 | 12, 13, 14, 15 | elpadd 39801 |
. . . . 5
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑝 ∈ (𝑋 + 𝑍) ↔ ((𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍) ∨ (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))))) |
| 17 | 7, 10, 11, 16 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ 𝑋 ⊆ 𝑌) → (𝑝 ∈ (𝑋 + 𝑍) ↔ ((𝑝 ∈ 𝑋 ∨ 𝑝 ∈ 𝑍) ∨ (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))))) |
| 18 | 12, 13, 14, 15 | elpadd 39801 |
. . . . 5
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑝 ∈ (𝑌 + 𝑍) ↔ ((𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍) ∨ (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑌 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))))) |
| 19 | 18 | adantr 480 |
. . . 4
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ 𝑋 ⊆ 𝑌) → (𝑝 ∈ (𝑌 + 𝑍) ↔ ((𝑝 ∈ 𝑌 ∨ 𝑝 ∈ 𝑍) ∨ (𝑝 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑌 ∃𝑟 ∈ 𝑍 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟))))) |
| 20 | 6, 17, 19 | 3imtr4d 294 |
. . 3
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ 𝑋 ⊆ 𝑌) → (𝑝 ∈ (𝑋 + 𝑍) → 𝑝 ∈ (𝑌 + 𝑍))) |
| 21 | 20 | ssrdv 3989 |
. 2
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ 𝑋 ⊆ 𝑌) → (𝑋 + 𝑍) ⊆ (𝑌 + 𝑍)) |
| 22 | 21 | ex 412 |
1
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 ⊆ 𝑌 → (𝑋 + 𝑍) ⊆ (𝑌 + 𝑍))) |