Step |
Hyp |
Ref |
Expression |
1 |
|
ssralv |
⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 ) ) |
3 |
2
|
ss2rabdv |
⊢ ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } ) |
4 |
3
|
adantl |
⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } ) |
5 |
|
ocval |
⊢ ( 𝐵 ⊆ ℋ → ( ⊥ ‘ 𝐵 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ) |
6 |
5
|
ad2antlr |
⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐵 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ) |
7 |
|
ocval |
⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } ) |
8 |
7
|
ad2antrr |
⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐴 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } ) |
9 |
4 6 8
|
3sstr4d |
⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) |
10 |
9
|
ex |
⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) ) |