Step |
Hyp |
Ref |
Expression |
1 |
|
padd0.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
2 |
|
padd0.p |
⊢ + = ( +𝑃 ‘ 𝐾 ) |
3 |
|
simpl |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → 𝐾 ∈ 𝐵 ) |
4 |
|
simpr |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → 𝑋 ⊆ 𝐴 ) |
5 |
|
0ss |
⊢ ∅ ⊆ 𝐴 |
6 |
5
|
a1i |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ∅ ⊆ 𝐴 ) |
7 |
3 4 6
|
3jca |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ ∅ ⊆ 𝐴 ) ) |
8 |
|
neirr |
⊢ ¬ ∅ ≠ ∅ |
9 |
8
|
intnan |
⊢ ¬ ( 𝑋 ≠ ∅ ∧ ∅ ≠ ∅ ) |
10 |
1 2
|
paddval0 |
⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ ∅ ⊆ 𝐴 ) ∧ ¬ ( 𝑋 ≠ ∅ ∧ ∅ ≠ ∅ ) ) → ( 𝑋 + ∅ ) = ( 𝑋 ∪ ∅ ) ) |
11 |
7 9 10
|
sylancl |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 + ∅ ) = ( 𝑋 ∪ ∅ ) ) |
12 |
|
un0 |
⊢ ( 𝑋 ∪ ∅ ) = 𝑋 |
13 |
11 12
|
eqtrdi |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 + ∅ ) = 𝑋 ) |