| Step | Hyp | Ref
| Expression |
| 1 | | atoml.1 |
. . . 4
⊢ 𝐴 ∈
Cℋ |
| 2 | 1 | hatomici 32378 |
. . 3
⊢ (𝐴 ≠ 0ℋ →
∃𝑥 ∈ HAtoms
𝑥 ⊆ 𝐴) |
| 3 | | nssne2 4047 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) → 𝑥 ≠ 𝐵) |
| 4 | 3 | adantrl 716 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴)) → 𝑥 ≠ 𝐵) |
| 5 | | atnemeq0 32396 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (𝑥 ≠ 𝐵 ↔ (𝑥 ∩ 𝐵) = 0ℋ)) |
| 6 | 4, 5 | imbitrid 244 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → ((𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴)) → (𝑥 ∩ 𝐵) = 0ℋ)) |
| 7 | | atelch 32363 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ HAtoms → 𝑥 ∈
Cℋ ) |
| 8 | | cvp 32394 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ HAtoms) → ((𝑥 ∩ 𝐵) = 0ℋ ↔ 𝑥 ⋖ℋ
(𝑥 ∨ℋ
𝐵))) |
| 9 | | atelch 32363 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ HAtoms → 𝐵 ∈
Cℋ ) |
| 10 | | chjcom 31525 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑥
∨ℋ 𝐵) =
(𝐵 ∨ℋ
𝑥)) |
| 11 | 9, 10 | sylan2 593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ HAtoms) → (𝑥 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝑥)) |
| 12 | 11 | breq2d 5155 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ HAtoms) → (𝑥 ⋖ℋ (𝑥 ∨ℋ 𝐵) ↔ 𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥))) |
| 13 | 8, 12 | bitrd 279 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ HAtoms) → ((𝑥 ∩ 𝐵) = 0ℋ ↔ 𝑥 ⋖ℋ
(𝐵 ∨ℋ
𝑥))) |
| 14 | 7, 13 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → ((𝑥 ∩ 𝐵) = 0ℋ ↔ 𝑥 ⋖ℋ
(𝐵 ∨ℋ
𝑥))) |
| 15 | 6, 14 | sylibd 239 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → ((𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴)) → 𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥))) |
| 16 | 15 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → ((𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴)) → 𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥))) |
| 17 | 16 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) → ((𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴)) → 𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥))) |
| 18 | 17 | imp 406 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴))) → 𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥)) |
| 19 | | chub1 31526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ 𝐵 ⊆ (𝐵 ∨ℋ 𝑥)) |
| 20 | 9, 7, 19 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → 𝐵 ⊆ (𝐵 ∨ℋ 𝑥)) |
| 21 | 20 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → 𝐵 ⊆ (𝐵 ∨ℋ 𝑥)) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → 𝐵 ⊆ (𝐵 ∨ℋ 𝑥)) |
| 23 | | pssss 4098 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → 𝐴 ⊆ (𝐵 ∨ℋ 𝐶)) |
| 24 | | sstr 3992 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝐵 ∨ℋ 𝐶)) → 𝑥 ⊆ (𝐵 ∨ℋ 𝐶)) |
| 25 | 23, 24 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶)) → 𝑥 ⊆ (𝐵 ∨ℋ 𝐶)) |
| 26 | 25 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶)) → 𝑥 ⊆ (𝐵 ∨ℋ 𝐶)) |
| 27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → 𝑥 ⊆ (𝐵 ∨ℋ 𝐶)) |
| 28 | | incom 4209 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∩ 𝑥) = (𝑥 ∩ 𝐵) |
| 29 | 3, 5 | imbitrid 244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) → (𝑥 ∩ 𝐵) = 0ℋ)) |
| 30 | 29 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) → (𝑥 ∩ 𝐵) = 0ℋ)) |
| 31 | 30 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) → (𝑥 ∩ 𝐵) = 0ℋ)) |
| 32 | 31 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴)) → (𝑥 ∩ 𝐵) = 0ℋ) |
| 33 | 28, 32 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴)) → (𝐵 ∩ 𝑥) = 0ℋ) |
| 34 | 33 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (𝐵 ∩ 𝑥) = 0ℋ) |
| 35 | | atexch 32400 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝑥 ⊆ (𝐵 ∨ℋ 𝐶) ∧ (𝐵 ∩ 𝑥) = 0ℋ) → 𝐶 ⊆ (𝐵 ∨ℋ 𝑥))) |
| 36 | 9, 35 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝑥 ⊆ (𝐵 ∨ℋ 𝐶) ∧ (𝐵 ∩ 𝑥) = 0ℋ) → 𝐶 ⊆ (𝐵 ∨ℋ 𝑥))) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → ((𝑥 ⊆ (𝐵 ∨ℋ 𝐶) ∧ (𝐵 ∩ 𝑥) = 0ℋ) → 𝐶 ⊆ (𝐵 ∨ℋ 𝑥))) |
| 38 | 27, 34, 37 | mp2and 699 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → 𝐶 ⊆ (𝐵 ∨ℋ 𝑥)) |
| 39 | | atelch 32363 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐶 ∈ HAtoms → 𝐶 ∈
Cℋ ) |
| 40 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → 𝐵 ∈ Cℋ
) |
| 41 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → 𝐶 ∈ Cℋ
) |
| 42 | | chjcl 31376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐵
∨ℋ 𝑥)
∈ Cℋ ) |
| 43 | 42 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (𝐵 ∨ℋ 𝑥) ∈ Cℋ
) |
| 44 | 40, 41, 43 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝑥) ∈ Cℋ
)) |
| 45 | 9, 7, 39, 44 | syl3an 1161 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ
∧ (𝐵
∨ℋ 𝑥)
∈ Cℋ )) |
| 46 | | chlub 31528 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ
∧ (𝐵
∨ℋ 𝑥)
∈ Cℋ ) → ((𝐵 ⊆ (𝐵 ∨ℋ 𝑥) ∧ 𝐶 ⊆ (𝐵 ∨ℋ 𝑥)) ↔ (𝐵 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝑥))) |
| 47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐵 ⊆ (𝐵 ∨ℋ 𝑥) ∧ 𝐶 ⊆ (𝐵 ∨ℋ 𝑥)) ↔ (𝐵 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝑥))) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → ((𝐵 ⊆ (𝐵 ∨ℋ 𝑥) ∧ 𝐶 ⊆ (𝐵 ∨ℋ 𝑥)) ↔ (𝐵 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝑥))) |
| 49 | 22, 38, 48 | mpbi2and 712 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (𝐵 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝑥)) |
| 50 | | chub1 31526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ 𝐵 ⊆ (𝐵 ∨ℋ 𝐶)) |
| 51 | 50 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → 𝐵 ⊆ (𝐵 ∨ℋ 𝐶)) |
| 52 | 51, 26 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (𝐵 ⊆ (𝐵 ∨ℋ 𝐶) ∧ 𝑥 ⊆ (𝐵 ∨ℋ 𝐶))) |
| 53 | | chjcl 31376 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐵
∨ℋ 𝐶)
∈ Cℋ ) |
| 54 | 53 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (𝐵 ∨ℋ 𝐶) ∈ Cℋ
) |
| 55 | | chlub 31528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ (𝐵
∨ℋ 𝐶)
∈ Cℋ ) → ((𝐵 ⊆ (𝐵 ∨ℋ 𝐶) ∧ 𝑥 ⊆ (𝐵 ∨ℋ 𝐶)) ↔ (𝐵 ∨ℋ 𝑥) ⊆ (𝐵 ∨ℋ 𝐶))) |
| 56 | 54, 55 | syld3an3 1411 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → ((𝐵 ⊆ (𝐵 ∨ℋ 𝐶) ∧ 𝑥 ⊆ (𝐵 ∨ℋ 𝐶)) ↔ (𝐵 ∨ℋ 𝑥) ⊆ (𝐵 ∨ℋ 𝐶))) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → ((𝐵 ⊆ (𝐵 ∨ℋ 𝐶) ∧ 𝑥 ⊆ (𝐵 ∨ℋ 𝐶)) ↔ (𝐵 ∨ℋ 𝑥) ⊆ (𝐵 ∨ℋ 𝐶))) |
| 58 | 52, 57 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (𝐵 ∨ℋ 𝑥) ⊆ (𝐵 ∨ℋ 𝐶)) |
| 59 | 9, 7, 39, 58 | syl3anl 1417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (𝐵 ∨ℋ 𝑥) ⊆ (𝐵 ∨ℋ 𝐶)) |
| 60 | 49, 59 | eqssd 4001 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (𝐵 ∨ℋ 𝐶) = (𝐵 ∨ℋ 𝑥)) |
| 61 | 60 | anassrs 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴)) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶)) → (𝐵 ∨ℋ 𝐶) = (𝐵 ∨ℋ 𝑥)) |
| 62 | 61 | psseq2d 4096 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴)) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶)) → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ↔ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥))) |
| 63 | 62 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴)) → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ↔ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)))) |
| 64 | 63 | ibd 269 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ ¬ 𝐵 ⊆ 𝐴)) → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → 𝐴 ⊊ (𝐵 ∨ℋ 𝑥))) |
| 65 | 64 | exp32 420 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝑥 ⊆ 𝐴 → (¬ 𝐵 ⊆ 𝐴 → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → 𝐴 ⊊ (𝐵 ∨ℋ 𝑥))))) |
| 66 | 65 | 3expa 1119 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) ∧ 𝐶 ∈ HAtoms) → (𝑥 ⊆ 𝐴 → (¬ 𝐵 ⊆ 𝐴 → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → 𝐴 ⊊ (𝐵 ∨ℋ 𝑥))))) |
| 67 | 66 | an32s 652 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) → (𝑥 ⊆ 𝐴 → (¬ 𝐵 ⊆ 𝐴 → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → 𝐴 ⊊ (𝐵 ∨ℋ 𝑥))))) |
| 68 | 67 | com34 91 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) → (𝑥 ⊆ 𝐴 → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ⊊ (𝐵 ∨ℋ 𝑥))))) |
| 69 | 68 | imp45 429 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴))) → 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)) |
| 70 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ 𝑥 ∈
Cℋ ) |
| 71 | 70, 42 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝑥 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝑥) ∈ Cℋ
)) |
| 72 | 9, 7, 71 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → (𝑥 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝑥) ∈ Cℋ
)) |
| 73 | | cvnbtwn3 32307 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝑥) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) → (𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥) → ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)) → 𝐴 = 𝑥))) |
| 74 | 1, 73 | mp3an3 1452 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝑥) ∈ Cℋ )
→ (𝑥
⋖ℋ (𝐵 ∨ℋ 𝑥) → ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)) → 𝐴 = 𝑥))) |
| 75 | 74 | exp4a 431 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝑥) ∈ Cℋ )
→ (𝑥
⋖ℋ (𝐵 ∨ℋ 𝑥) → (𝑥 ⊆ 𝐴 → (𝐴 ⊊ (𝐵 ∨ℋ 𝑥) → 𝐴 = 𝑥)))) |
| 76 | 75 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝑥) ∈ Cℋ )
→ (𝑥 ⊆ 𝐴 → (𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥) → (𝐴 ⊊ (𝐵 ∨ℋ 𝑥) → 𝐴 = 𝑥)))) |
| 77 | 76 | imp4a 422 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝑥) ∈ Cℋ )
→ (𝑥 ⊆ 𝐴 → ((𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)) → 𝐴 = 𝑥))) |
| 78 | 72, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → (𝑥 ⊆ 𝐴 → ((𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)) → 𝐴 = 𝑥))) |
| 79 | 78 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) → (𝑥 ⊆ 𝐴 → ((𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)) → 𝐴 = 𝑥))) |
| 80 | 79 | imp 406 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) ∧ 𝑥 ⊆ 𝐴) → ((𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)) → 𝐴 = 𝑥)) |
| 81 | 80 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴))) → ((𝑥 ⋖ℋ (𝐵 ∨ℋ 𝑥) ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝑥)) → 𝐴 = 𝑥)) |
| 82 | 18, 69, 81 | mp2and 699 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴))) → 𝐴 = 𝑥) |
| 83 | 82 | eleq1d 2826 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴))) → (𝐴 ∈ HAtoms ↔ 𝑥 ∈ HAtoms)) |
| 84 | 83 | biimprcd 250 |
. . . . . . . 8
⊢ (𝑥 ∈ HAtoms → ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) ∧ (𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴))) → 𝐴 ∈ HAtoms)) |
| 85 | 84 | exp4c 432 |
. . . . . . 7
⊢ (𝑥 ∈ HAtoms → ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝑥 ∈ HAtoms → ((𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴)) → 𝐴 ∈ HAtoms)))) |
| 86 | 85 | pm2.43b 55 |
. . . . . 6
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝑥 ∈ HAtoms → ((𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴)) → 𝐴 ∈ HAtoms))) |
| 87 | 86 | imp 406 |
. . . . 5
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) → ((𝑥 ⊆ 𝐴 ∧ (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) ∧ ¬ 𝐵 ⊆ 𝐴)) → 𝐴 ∈ HAtoms)) |
| 88 | 87 | exp4d 433 |
. . . 4
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝑥 ∈ HAtoms) → (𝑥 ⊆ 𝐴 → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms)))) |
| 89 | 88 | rexlimdva 3155 |
. . 3
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) →
(∃𝑥 ∈ HAtoms
𝑥 ⊆ 𝐴 → (𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms)))) |
| 90 | 2, 89 | syl5 34 |
. 2
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝐴 ≠ 0ℋ →
(𝐴 ⊊ (𝐵 ∨ℋ 𝐶) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms)))) |
| 91 | 90 | imp32 418 |
1
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝐴 ≠ 0ℋ ∧
𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms)) |