Proof of Theorem atcvat4i
Step | Hyp | Ref
| Expression |
1 | | atcvat3.1 |
. . . . . . . . 9
⊢ 𝐴 ∈
Cℋ |
2 | 1 | hatomici 30721 |
. . . . . . . 8
⊢ (𝐴 ≠ 0ℋ →
∃𝑥 ∈ HAtoms
𝑥 ⊆ 𝐴) |
3 | | atelch 30706 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ HAtoms → 𝐶 ∈
Cℋ ) |
4 | | atelch 30706 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ HAtoms → 𝑥 ∈
Cℋ ) |
5 | | chub1 29869 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ 𝐶 ⊆ (𝐶 ∨ℋ 𝑥)) |
6 | 3, 4, 5 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → 𝐶 ⊆ (𝐶 ∨ℋ 𝑥)) |
7 | | sseq1 3946 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = 𝐶 → (𝐵 ⊆ (𝐶 ∨ℋ 𝑥) ↔ 𝐶 ⊆ (𝐶 ∨ℋ 𝑥))) |
8 | 6, 7 | syl5ibr 245 |
. . . . . . . . . . . . 13
⊢ (𝐵 = 𝐶 → ((𝐶 ∈ HAtoms ∧ 𝑥 ∈ HAtoms) → 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))) |
9 | 8 | expd 416 |
. . . . . . . . . . . 12
⊢ (𝐵 = 𝐶 → (𝐶 ∈ HAtoms → (𝑥 ∈ HAtoms → 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))) |
10 | 9 | impcom 408 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶) → (𝑥 ∈ HAtoms → 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))) |
11 | 10 | anim2d 612 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ∈ HAtoms) → (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))) |
12 | 11 | expcomd 417 |
. . . . . . . . 9
⊢ ((𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶) → (𝑥 ∈ HAtoms → (𝑥 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))) |
13 | 12 | reximdvai 3200 |
. . . . . . . 8
⊢ ((𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶) → (∃𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴 → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))) |
14 | 2, 13 | syl5 34 |
. . . . . . 7
⊢ ((𝐶 ∈ HAtoms ∧ 𝐵 = 𝐶) → (𝐴 ≠ 0ℋ →
∃𝑥 ∈ HAtoms
(𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))) |
15 | 14 | ex 413 |
. . . . . 6
⊢ (𝐶 ∈ HAtoms → (𝐵 = 𝐶 → (𝐴 ≠ 0ℋ →
∃𝑥 ∈ HAtoms
(𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))) |
16 | 15 | a1i 11 |
. . . . 5
⊢ (𝐵 ⊆ (𝐴 ∨ℋ 𝐶) → (𝐶 ∈ HAtoms → (𝐵 = 𝐶 → (𝐴 ≠ 0ℋ →
∃𝑥 ∈ HAtoms
(𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))))) |
17 | 16 | com4l 92 |
. . . 4
⊢ (𝐶 ∈ HAtoms → (𝐵 = 𝐶 → (𝐴 ≠ 0ℋ → (𝐵 ⊆ (𝐴 ∨ℋ 𝐶) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))))) |
18 | 17 | imp4a 423 |
. . 3
⊢ (𝐶 ∈ HAtoms → (𝐵 = 𝐶 → ((𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))) |
19 | 18 | adantl 482 |
. 2
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝐵 = 𝐶 → ((𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))) |
20 | | atelch 30706 |
. . . . . . . 8
⊢ (𝐵 ∈ HAtoms → 𝐵 ∈
Cℋ ) |
21 | | chlejb2 29875 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝐶 ⊆ 𝐴 ↔ (𝐴 ∨ℋ 𝐶) = 𝐴)) |
22 | 1, 21 | mpan2 688 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈
Cℋ → (𝐶 ⊆ 𝐴 ↔ (𝐴 ∨ℋ 𝐶) = 𝐴)) |
23 | 22 | biimpa 477 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈
Cℋ ∧ 𝐶 ⊆ 𝐴) → (𝐴 ∨ℋ 𝐶) = 𝐴) |
24 | 23 | sseq2d 3953 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈
Cℋ ∧ 𝐶 ⊆ 𝐴) → (𝐵 ⊆ (𝐴 ∨ℋ 𝐶) ↔ 𝐵 ⊆ 𝐴)) |
25 | 24 | biimpa 477 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈
Cℋ ∧ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → 𝐵 ⊆ 𝐴) |
26 | 25 | expl 458 |
. . . . . . . . . 10
⊢ (𝐶 ∈
Cℋ → ((𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → 𝐵 ⊆ 𝐴)) |
27 | 26 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → 𝐵 ⊆ 𝐴)) |
28 | | chub2 29870 |
. . . . . . . . 9
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ 𝐵 ⊆ (𝐶 ∨ℋ 𝐵)) |
29 | 27, 28 | jctird 527 |
. . . . . . . 8
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝐵)))) |
30 | 20, 3, 29 | syl2an 596 |
. . . . . . 7
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝐵)))) |
31 | | simpl 483 |
. . . . . . 7
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → 𝐵 ∈ HAtoms) |
32 | 30, 31 | jctild 526 |
. . . . . 6
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐶 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → (𝐵 ∈ HAtoms ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝐵))))) |
33 | 32 | impl 456 |
. . . . 5
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → (𝐵 ∈ HAtoms ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝐵)))) |
34 | | sseq1 3946 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
35 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐶 ∨ℋ 𝑥) = (𝐶 ∨ℋ 𝐵)) |
36 | 35 | sseq2d 3953 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐵 ⊆ (𝐶 ∨ℋ 𝑥) ↔ 𝐵 ⊆ (𝐶 ∨ℋ 𝐵))) |
37 | 34, 36 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)) ↔ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝐵)))) |
38 | 37 | rspcev 3561 |
. . . . 5
⊢ ((𝐵 ∈ HAtoms ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝐵))) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))) |
39 | 33, 38 | syl 17 |
. . . 4
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))) |
40 | 39 | adantrl 713 |
. . 3
⊢ ((((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝐶 ⊆ 𝐴) ∧ (𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))) |
41 | 40 | exp31 420 |
. 2
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝐶 ⊆ 𝐴 → ((𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))) |
42 | | simpr 485 |
. . 3
⊢ ((𝐴 ≠ 0ℋ ∧
𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) |
43 | | ioran 981 |
. . . 4
⊢ (¬
(𝐵 = 𝐶 ∨ 𝐶 ⊆ 𝐴) ↔ (¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴)) |
44 | 1 | atcvat3i 30758 |
. . . . . . 7
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ HAtoms)) |
45 | 3 | ad2antlr 724 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → 𝐶 ∈ Cℋ
) |
46 | 44 | imp 407 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ HAtoms) |
47 | | simpll 764 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → 𝐵 ∈ HAtoms) |
48 | 45, 46, 47 | 3jca 1127 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → (𝐶 ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ HAtoms ∧ 𝐵 ∈
HAtoms)) |
49 | | inss2 4163 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ (𝐵 ∨ℋ 𝐶) |
50 | | chjcom 29868 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐵
∨ℋ 𝐶) =
(𝐶 ∨ℋ
𝐵)) |
51 | 20, 3, 50 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝐵 ∨ℋ 𝐶) = (𝐶 ∨ℋ 𝐵)) |
52 | 49, 51 | sseqtrid 3973 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ (𝐶 ∨ℋ 𝐵)) |
53 | 52 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ (𝐶 ∨ℋ 𝐵)) |
54 | | atnssm0 30738 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ HAtoms) → (¬ 𝐶 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐶) = 0ℋ)) |
55 | 1, 54 | mpan 687 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ HAtoms → (¬
𝐶 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐶) = 0ℋ)) |
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (¬
𝐶 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐶) = 0ℋ)) |
57 | | inss1 4162 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ 𝐴 |
58 | | sslin 4168 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ 𝐴 → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ⊆ (𝐶 ∩ 𝐴)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ⊆ (𝐶 ∩ 𝐴) |
60 | | incom 4135 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶) |
61 | 59, 60 | sseqtri 3957 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ⊆ (𝐴 ∩ 𝐶) |
62 | | sseq2 3947 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∩ 𝐶) = 0ℋ → ((𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ⊆ (𝐴 ∩ 𝐶) ↔ (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ⊆
0ℋ)) |
63 | 61, 62 | mpbii 232 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∩ 𝐶) = 0ℋ → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ⊆
0ℋ) |
64 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ 𝐶 ∈
Cℋ ) |
65 | | chjcl 29719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐵
∨ℋ 𝐶)
∈ Cℋ ) |
66 | | chincl 29861 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝐶) ∈ Cℋ )
→ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Cℋ ) |
67 | 1, 65, 66 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Cℋ ) |
68 | | chincl 29861 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 ∈
Cℋ ∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ Cℋ
) → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ∈ Cℋ
) |
69 | 64, 67, 68 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ∈ Cℋ
) |
70 | 20, 3, 69 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ∈ Cℋ
) |
71 | | chle0 29805 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ∈ Cℋ
→ ((𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ⊆ 0ℋ ↔
(𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) ⊆ 0ℋ ↔
(𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ)) |
73 | 63, 72 | syl5ib 243 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐴 ∩ 𝐶) = 0ℋ → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ)) |
74 | 56, 73 | sylbid 239 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (¬
𝐶 ⊆ 𝐴 → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ)) |
75 | 74 | imp 407 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ¬
𝐶 ⊆ 𝐴) → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ) |
76 | 75 | adantrl 713 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴)) → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ) |
77 | 76 | adantrr 714 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ) |
78 | 53, 77 | jca 512 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ (𝐶 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ)) |
79 | | atexch 30743 |
. . . . . . . . . 10
⊢ ((𝐶 ∈
Cℋ ∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ (𝐶 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) = 0ℋ) → 𝐵 ⊆ (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))))) |
80 | 48, 78, 79 | sylc 65 |
. . . . . . . . 9
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → 𝐵 ⊆ (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)))) |
81 | 80, 57 | jctil 520 |
. . . . . . . 8
⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶))) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))))) |
82 | 81 | ex 413 |
. . . . . . 7
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)))))) |
83 | 44, 82 | jcad 513 |
. . . . . 6
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ HAtoms ∧ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))))))) |
84 | | sseq1 3946 |
. . . . . . . 8
⊢ (𝑥 = (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) → (𝑥 ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ 𝐴)) |
85 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) → (𝐶 ∨ℋ 𝑥) = (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)))) |
86 | 85 | sseq2d 3953 |
. . . . . . . 8
⊢ (𝑥 = (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) → (𝐵 ⊆ (𝐶 ∨ℋ 𝑥) ↔ 𝐵 ⊆ (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))))) |
87 | 84, 86 | anbi12d 631 |
. . . . . . 7
⊢ (𝑥 = (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) → ((𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)) ↔ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)))))) |
88 | 87 | rspcev 3561 |
. . . . . 6
⊢ (((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ HAtoms ∧ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))))) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))) |
89 | 83, 88 | syl6 35 |
. . . . 5
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))) |
90 | 89 | expd 416 |
. . . 4
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((¬
𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) → (𝐵 ⊆ (𝐴 ∨ℋ 𝐶) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))) |
91 | 43, 90 | syl5bi 241 |
. . 3
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (¬
(𝐵 = 𝐶 ∨ 𝐶 ⊆ 𝐴) → (𝐵 ⊆ (𝐴 ∨ℋ 𝐶) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))) |
92 | 42, 91 | syl7 74 |
. 2
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (¬
(𝐵 = 𝐶 ∨ 𝐶 ⊆ 𝐴) → ((𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥))))) |
93 | 19, 41, 92 | ecase3d 1031 |
1
⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐴 ≠ 0ℋ ∧
𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))) |