Step |
Hyp |
Ref |
Expression |
1 |
|
elat2 |
⊢ ( 𝐵 ∈ HAtoms ↔ ( 𝐵 ∈ Cℋ ∧ ( 𝐵 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( 𝑥 = 𝐵 ∨ 𝑥 = 0ℋ ) ) ) ) ) |
2 |
|
sseq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵 ) ) |
3 |
|
eqeq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐵 ↔ 𝐴 = 𝐵 ) ) |
4 |
|
eqeq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 0ℋ ↔ 𝐴 = 0ℋ ) ) |
5 |
3 4
|
orbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐵 ∨ 𝑥 = 0ℋ ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) ) |
6 |
2 5
|
imbi12d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ⊆ 𝐵 → ( 𝑥 = 𝐵 ∨ 𝑥 = 0ℋ ) ) ↔ ( 𝐴 ⊆ 𝐵 → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) ) ) |
7 |
6
|
rspcv |
⊢ ( 𝐴 ∈ Cℋ → ( ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( 𝑥 = 𝐵 ∨ 𝑥 = 0ℋ ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) ) ) |
8 |
7
|
adantld |
⊢ ( 𝐴 ∈ Cℋ → ( ( 𝐵 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( 𝑥 = 𝐵 ∨ 𝑥 = 0ℋ ) ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) ) ) |
9 |
8
|
adantld |
⊢ ( 𝐴 ∈ Cℋ → ( ( 𝐵 ∈ Cℋ ∧ ( 𝐵 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( 𝑥 = 𝐵 ∨ 𝑥 = 0ℋ ) ) ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) ) ) |
10 |
9
|
imp |
⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐵 ∈ Cℋ ∧ ( 𝐵 ≠ 0ℋ ∧ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ 𝐵 → ( 𝑥 = 𝐵 ∨ 𝑥 = 0ℋ ) ) ) ) ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) ) |
11 |
1 10
|
sylan2b |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⊆ 𝐵 → ( 𝐴 = 𝐵 ∨ 𝐴 = 0ℋ ) ) ) |