Step |
Hyp |
Ref |
Expression |
1 |
|
sstr2 |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ 𝑥 → 𝐴 ⊆ 𝑥 ) ) |
2 |
1
|
ralrimivw |
⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∈ Sℋ ( 𝐵 ⊆ 𝑥 → 𝐴 ⊆ 𝑥 ) ) |
3 |
|
ss2rab |
⊢ ( { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ↔ ∀ 𝑥 ∈ Sℋ ( 𝐵 ⊆ 𝑥 → 𝐴 ⊆ 𝑥 ) ) |
4 |
2 3
|
sylibr |
⊢ ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ) |
5 |
|
intss |
⊢ ( { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ⊆ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ) |
6 |
4 5
|
syl |
⊢ ( 𝐴 ⊆ 𝐵 → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ) |
7 |
6
|
adantl |
⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ) |
8 |
|
sstr |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℋ ) → 𝐴 ⊆ ℋ ) |
9 |
8
|
ancoms |
⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ ℋ ) |
10 |
|
spanval |
⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ) |
11 |
9 10
|
syl |
⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ) |
12 |
|
spanval |
⊢ ( 𝐵 ⊆ ℋ → ( span ‘ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ) |
13 |
12
|
adantr |
⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐵 ⊆ 𝑥 } ) |
14 |
7 11 13
|
3sstr4d |
⊢ ( ( 𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵 ) → ( span ‘ 𝐴 ) ⊆ ( span ‘ 𝐵 ) ) |