| Step | Hyp | Ref
| Expression |
| 1 | | atoml.1 |
. . . . . . . . 9
⊢ 𝐴 ∈
Cℋ |
| 2 | | atelch 32363 |
. . . . . . . . 9
⊢ (𝐵 ∈ HAtoms → 𝐵 ∈
Cℋ ) |
| 3 | | chjcl 31376 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
∨ℋ 𝐵)
∈ Cℋ ) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . . . . 8
⊢ (𝐵 ∈ HAtoms → (𝐴 ∨ℋ 𝐵) ∈
Cℋ ) |
| 5 | 1 | choccli 31326 |
. . . . . . . 8
⊢
(⊥‘𝐴)
∈ Cℋ |
| 6 | | chincl 31518 |
. . . . . . . 8
⊢ (((𝐴 ∨ℋ 𝐵) ∈
Cℋ ∧ (⊥‘𝐴) ∈ Cℋ )
→ ((𝐴
∨ℋ 𝐵)
∩ (⊥‘𝐴))
∈ Cℋ ) |
| 7 | 4, 5, 6 | sylancl 586 |
. . . . . . 7
⊢ (𝐵 ∈ HAtoms → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈
Cℋ ) |
| 8 | | hatomic 32379 |
. . . . . . 7
⊢ ((((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈
Cℋ ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ) →
∃𝑥 ∈ HAtoms
𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) |
| 9 | 7, 8 | sylan 580 |
. . . . . 6
⊢ ((𝐵 ∈ HAtoms ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)
→ ∃𝑥 ∈
HAtoms 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) |
| 10 | | atelch 32363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ HAtoms → 𝑥 ∈
Cℋ ) |
| 11 | | inss2 4238 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ⊆ (⊥‘𝐴) |
| 12 | | sstr 3992 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ⊆ (⊥‘𝐴)) → 𝑥 ⊆ (⊥‘𝐴)) |
| 13 | 11, 12 | mpan2 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) → 𝑥 ⊆ (⊥‘𝐴)) |
| 14 | 1 | pjococi 31456 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(⊥‘(⊥‘𝐴)) = 𝐴 |
| 15 | 14 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊥‘(⊥‘𝐴)) ∨ℋ 𝑥) = (𝐴 ∨ℋ 𝑥) |
| 16 | 15 | ineq1i 4216 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊥‘(⊥‘𝐴)) ∨ℋ 𝑥) ∩ (⊥‘𝐴)) = ((𝐴 ∨ℋ 𝑥) ∩ (⊥‘𝐴)) |
| 17 | | incom 4209 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊥‘(⊥‘𝐴)) ∨ℋ 𝑥) ∩ (⊥‘𝐴)) = ((⊥‘𝐴) ∩ ((⊥‘(⊥‘𝐴)) ∨ℋ 𝑥)) |
| 18 | 16, 17 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∨ℋ 𝑥) ∩ (⊥‘𝐴)) = ((⊥‘𝐴) ∩
((⊥‘(⊥‘𝐴)) ∨ℋ 𝑥)) |
| 19 | | pjoml3 31631 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊥‘𝐴)
∈ Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝑥 ⊆
(⊥‘𝐴) →
((⊥‘𝐴) ∩
((⊥‘(⊥‘𝐴)) ∨ℋ 𝑥)) = 𝑥)) |
| 20 | 5, 19 | mpan 690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ (⊥‘𝐴) → ((⊥‘𝐴) ∩ ((⊥‘(⊥‘𝐴)) ∨ℋ 𝑥)) = 𝑥)) |
| 21 | 20 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (⊥‘𝐴)) → ((⊥‘𝐴) ∩ ((⊥‘(⊥‘𝐴)) ∨ℋ 𝑥)) = 𝑥) |
| 22 | 18, 21 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (⊥‘𝐴)) → ((𝐴 ∨ℋ 𝑥) ∩ (⊥‘𝐴)) = 𝑥) |
| 23 | 10, 13, 22 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ HAtoms ∧ 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) → ((𝐴 ∨ℋ 𝑥) ∩ (⊥‘𝐴)) = 𝑥) |
| 24 | 23 | ad2ant2lr 748 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → ((𝐴 ∨ℋ 𝑥) ∩ (⊥‘𝐴)) = 𝑥) |
| 25 | | inss1 4237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ⊆ (𝐴 ∨ℋ 𝐵) |
| 26 | | sstr 3992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ⊆ (𝐴 ∨ℋ 𝐵)) → 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) |
| 27 | 25, 26 | mpan2 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) → 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) |
| 28 | | chub1 31526 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)) |
| 29 | 1, 28 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ∈
Cℋ → 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)) |
| 31 | 1, 3 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈
Cℋ → (𝐴 ∨ℋ 𝐵) ∈ Cℋ
) |
| 32 | | chlub 31528 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ (𝐴
∨ℋ 𝐵)
∈ Cℋ ) → ((𝐴 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 33 | 1, 32 | mp3an1 1450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
→ ((𝐴 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 34 | 31, 33 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((𝐴 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 35 | 34 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((𝐴 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 36 | 35 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ ((𝐴 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 37 | 30, 36 | mpand 695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 38 | 2, 10, 37 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 39 | 38 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵)) |
| 40 | 27, 39 | sylan2 593 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵)) |
| 41 | 40 | adantrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵)) |
| 42 | | chjcl 31376 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) |
| 43 | 1, 10, 42 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ HAtoms → (𝐴 ∨ℋ 𝑥) ∈
Cℋ ) |
| 44 | 2, 43 | anim12i 613 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → (𝐵 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ
)) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → (𝐵 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ
)) |
| 46 | | chub1 31526 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ 𝐴 ⊆ (𝐴 ∨ℋ 𝑥)) |
| 47 | 1, 10, 46 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ HAtoms → 𝐴 ⊆ (𝐴 ∨ℋ 𝑥)) |
| 48 | 47 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → 𝐴 ⊆ (𝐴 ∨ℋ 𝑥)) |
| 49 | | pm3.22 459 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → (𝑥 ∈ HAtoms ∧ 𝐵 ∈
HAtoms)) |
| 50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → (𝑥 ∈ HAtoms ∧ 𝐵 ∈
HAtoms)) |
| 51 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ HAtoms ∧ 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) → 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) |
| 52 | | incom 4209 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∩ 𝑥) = (𝑥 ∩ 𝐴) |
| 53 | | chsh 31243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈
Cℋ → 𝑥 ∈ Sℋ
) |
| 54 | 1 | chshii 31246 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐴 ∈
Sℋ |
| 55 | | orthin 31465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈
Sℋ ∧ 𝐴 ∈ Sℋ )
→ (𝑥 ⊆
(⊥‘𝐴) →
(𝑥 ∩ 𝐴) = 0ℋ)) |
| 56 | 53, 54, 55 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ (⊥‘𝐴) → (𝑥 ∩ 𝐴) = 0ℋ)) |
| 57 | 56 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (⊥‘𝐴)) → (𝑥 ∩ 𝐴) = 0ℋ) |
| 58 | 52, 57 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (⊥‘𝐴)) → (𝐴 ∩ 𝑥) = 0ℋ) |
| 59 | 10, 13, 58 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ HAtoms ∧ 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) → (𝐴 ∩ 𝑥) = 0ℋ) |
| 60 | 51, 59 | jca 511 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ HAtoms ∧ 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) → (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐴 ∩ 𝑥) = 0ℋ)) |
| 61 | 60 | ad2ant2lr 748 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐴 ∩ 𝑥) = 0ℋ)) |
| 62 | | atexch 32400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐴 ∩ 𝑥) = 0ℋ) → 𝐵 ⊆ (𝐴 ∨ℋ 𝑥))) |
| 63 | 1, 62 | mp3an1 1450 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐴 ∩ 𝑥) = 0ℋ) → 𝐵 ⊆ (𝐴 ∨ℋ 𝑥))) |
| 64 | 50, 61, 63 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → 𝐵 ⊆ (𝐴 ∨ℋ 𝑥)) |
| 65 | | chlub 31528 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) → ((𝐴 ⊆ (𝐴 ∨ℋ 𝑥) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝑥)) ↔ (𝐴 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝑥))) |
| 66 | 1, 65 | mp3an1 1450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
→ ((𝐴 ⊆ (𝐴 ∨ℋ 𝑥) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝑥)) ↔ (𝐴 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝑥))) |
| 67 | 66 | biimpd 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
→ ((𝐴 ⊆ (𝐴 ∨ℋ 𝑥) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝑥)) → (𝐴 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝑥))) |
| 68 | 67 | expd 415 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
→ (𝐴 ⊆ (𝐴 ∨ℋ 𝑥) → (𝐵 ⊆ (𝐴 ∨ℋ 𝑥) → (𝐴 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝑥)))) |
| 69 | 45, 48, 64, 68 | syl3c 66 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → (𝐴 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝑥)) |
| 70 | 41, 69 | eqssd 4001 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → (𝐴 ∨ℋ 𝑥) = (𝐴 ∨ℋ 𝐵)) |
| 71 | 70 | ineq1d 4219 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → ((𝐴 ∨ℋ 𝑥) ∩ (⊥‘𝐴)) = ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) |
| 72 | 24, 71 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → 𝑥 = ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) |
| 73 | 72 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)) → (𝑥 ∈ HAtoms ↔ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈
HAtoms)) |
| 74 | 73 | exp43 436 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ HAtoms → (𝑥 ∈ HAtoms → (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) → (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ → (𝑥 ∈ HAtoms ↔ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈
HAtoms))))) |
| 75 | 74 | com24 95 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ HAtoms → (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ
→ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) → (𝑥 ∈ HAtoms → (𝑥 ∈ HAtoms ↔ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms))))) |
| 76 | 75 | imp31 417 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ HAtoms ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)
∧ 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) → (𝑥 ∈ HAtoms → (𝑥 ∈ HAtoms ↔ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms))) |
| 77 | 76 | ibd 269 |
. . . . . . . . 9
⊢ (((𝐵 ∈ HAtoms ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)
∧ 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴))) → (𝑥 ∈ HAtoms → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms)) |
| 78 | 77 | ex 412 |
. . . . . . . 8
⊢ ((𝐵 ∈ HAtoms ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)
→ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) → (𝑥 ∈ HAtoms → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms))) |
| 79 | 78 | com23 86 |
. . . . . . 7
⊢ ((𝐵 ∈ HAtoms ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)
→ (𝑥 ∈ HAtoms
→ (𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms))) |
| 80 | 79 | rexlimdv 3153 |
. . . . . 6
⊢ ((𝐵 ∈ HAtoms ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)
→ (∃𝑥 ∈
HAtoms 𝑥 ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms)) |
| 81 | 9, 80 | mpd 15 |
. . . . 5
⊢ ((𝐵 ∈ HAtoms ∧ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ)
→ ((𝐴
∨ℋ 𝐵)
∩ (⊥‘𝐴))
∈ HAtoms) |
| 82 | 81 | ex 412 |
. . . 4
⊢ (𝐵 ∈ HAtoms → (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ≠ 0ℋ
→ ((𝐴
∨ℋ 𝐵)
∩ (⊥‘𝐴))
∈ HAtoms)) |
| 83 | 82 | necon1bd 2958 |
. . 3
⊢ (𝐵 ∈ HAtoms → (¬
((𝐴 ∨ℋ
𝐵) ∩
(⊥‘𝐴)) ∈
HAtoms → ((𝐴
∨ℋ 𝐵)
∩ (⊥‘𝐴)) =
0ℋ)) |
| 84 | 83 | orrd 864 |
. 2
⊢ (𝐵 ∈ HAtoms → (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms ∨ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) =
0ℋ)) |
| 85 | | elun 4153 |
. . 3
⊢ (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ (HAtoms ∪
{0ℋ}) ↔ (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms ∨ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈
{0ℋ})) |
| 86 | | fvex 6919 |
. . . . . 6
⊢
(⊥‘𝐴)
∈ V |
| 87 | 86 | inex2 5318 |
. . . . 5
⊢ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ V |
| 88 | 87 | elsn 4641 |
. . . 4
⊢ (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ {0ℋ}
↔ ((𝐴
∨ℋ 𝐵)
∩ (⊥‘𝐴)) =
0ℋ) |
| 89 | 88 | orbi2i 913 |
. . 3
⊢ ((((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms ∨ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ {0ℋ})
↔ (((𝐴
∨ℋ 𝐵)
∩ (⊥‘𝐴))
∈ HAtoms ∨ ((𝐴
∨ℋ 𝐵)
∩ (⊥‘𝐴)) =
0ℋ)) |
| 90 | 85, 89 | bitri 275 |
. 2
⊢ (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ (HAtoms ∪
{0ℋ}) ↔ (((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms ∨ ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) = 0ℋ)) |
| 91 | 84, 90 | sylibr 234 |
1
⊢ (𝐵 ∈ HAtoms → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ (HAtoms ∪
{0ℋ})) |