| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | neanior 3035 | . . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ↔ ¬
(𝑋 = ∅ ∨ 𝑌 = ∅)) | 
| 2 | 1 | bicomi 224 | . . 3
⊢ (¬
(𝑋 = ∅ ∨ 𝑌 = ∅) ↔ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) | 
| 3 | 2 | con1bii 356 | . 2
⊢ (¬
(𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ↔ (𝑋 = ∅ ∨ 𝑌 = ∅)) | 
| 4 |  | eqid 2737 | . . . 4
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 5 |  | eqid 2737 | . . . 4
⊢
(join‘𝐾) =
(join‘𝐾) | 
| 6 |  | padd0.a | . . . 4
⊢ 𝐴 = (Atoms‘𝐾) | 
| 7 |  | padd0.p | . . . 4
⊢  + =
(+𝑃‘𝐾) | 
| 8 | 4, 5, 6, 7 | elpadd 39801 | . . 3
⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑆 ∈ (𝑋 + 𝑌) ↔ ((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ∨ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟))))) | 
| 9 |  | rex0 4360 | . . . . . . . 8
⊢  ¬
∃𝑞 ∈ ∅
∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟) | 
| 10 |  | rexeq 3322 | . . . . . . . 8
⊢ (𝑋 = ∅ → (∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟) ↔ ∃𝑞 ∈ ∅ ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟))) | 
| 11 | 9, 10 | mtbiri 327 | . . . . . . 7
⊢ (𝑋 = ∅ → ¬
∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)) | 
| 12 |  | rex0 4360 | . . . . . . . . . 10
⊢  ¬
∃𝑟 ∈ ∅
𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟) | 
| 13 | 12 | a1i 11 | . . . . . . . . 9
⊢ (𝑞 ∈ 𝑋 → ¬ ∃𝑟 ∈ ∅ 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)) | 
| 14 | 13 | nrex 3074 | . . . . . . . 8
⊢  ¬
∃𝑞 ∈ 𝑋 ∃𝑟 ∈ ∅ 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟) | 
| 15 |  | rexeq 3322 | . . . . . . . . 9
⊢ (𝑌 = ∅ → (∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟) ↔ ∃𝑟 ∈ ∅ 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟))) | 
| 16 | 15 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑌 = ∅ → (∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟) ↔ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ ∅ 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟))) | 
| 17 | 14, 16 | mtbiri 327 | . . . . . . 7
⊢ (𝑌 = ∅ → ¬
∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)) | 
| 18 | 11, 17 | jaoi 858 | . . . . . 6
⊢ ((𝑋 = ∅ ∨ 𝑌 = ∅) → ¬
∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)) | 
| 19 | 18 | intnand 488 | . . . . 5
⊢ ((𝑋 = ∅ ∨ 𝑌 = ∅) → ¬ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟))) | 
| 20 |  | biorf 937 | . . . . 5
⊢ (¬
(𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)) → ((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ↔ ((𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)) ∨ (𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌)))) | 
| 21 | 19, 20 | syl 17 | . . . 4
⊢ ((𝑋 = ∅ ∨ 𝑌 = ∅) → ((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ↔ ((𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)) ∨ (𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌)))) | 
| 22 |  | orcom 871 | . . . 4
⊢ (((𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)) ∨ (𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌)) ↔ ((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ∨ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟)))) | 
| 23 | 21, 22 | bitr2di 288 | . . 3
⊢ ((𝑋 = ∅ ∨ 𝑌 = ∅) → (((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ∨ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆(le‘𝐾)(𝑞(join‘𝐾)𝑟))) ↔ (𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌))) | 
| 24 | 8, 23 | sylan9bb 509 | . 2
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 = ∅ ∨ 𝑌 = ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌))) | 
| 25 | 3, 24 | sylan2b 594 | 1
⊢ (((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ ¬ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌))) |