Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hilex |
⊢ ℋ ∈ V |
2 |
1
|
elpw2 |
⊢ ( 𝐻 ∈ 𝒫 ℋ ↔ 𝐻 ⊆ ℋ ) |
3 |
|
3anass |
⊢ ( ( 0ℎ ∈ 𝐻 ∧ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ↔ ( 0ℎ ∈ 𝐻 ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ) |
4 |
2 3
|
anbi12i |
⊢ ( ( 𝐻 ∈ 𝒫 ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ↔ ( 𝐻 ⊆ ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ) ) |
5 |
|
eleq2 |
⊢ ( ℎ = 𝐻 → ( 0ℎ ∈ ℎ ↔ 0ℎ ∈ 𝐻 ) ) |
6 |
|
id |
⊢ ( ℎ = 𝐻 → ℎ = 𝐻 ) |
7 |
6
|
sqxpeqd |
⊢ ( ℎ = 𝐻 → ( ℎ × ℎ ) = ( 𝐻 × 𝐻 ) ) |
8 |
7
|
imaeq2d |
⊢ ( ℎ = 𝐻 → ( +ℎ “ ( ℎ × ℎ ) ) = ( +ℎ “ ( 𝐻 × 𝐻 ) ) ) |
9 |
8 6
|
sseq12d |
⊢ ( ℎ = 𝐻 → ( ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ↔ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ) ) |
10 |
|
xpeq2 |
⊢ ( ℎ = 𝐻 → ( ℂ × ℎ ) = ( ℂ × 𝐻 ) ) |
11 |
10
|
imaeq2d |
⊢ ( ℎ = 𝐻 → ( ·ℎ “ ( ℂ × ℎ ) ) = ( ·ℎ “ ( ℂ × 𝐻 ) ) ) |
12 |
11 6
|
sseq12d |
⊢ ( ℎ = 𝐻 → ( ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ↔ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) |
13 |
5 9 12
|
3anbi123d |
⊢ ( ℎ = 𝐻 → ( ( 0ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ) ↔ ( 0ℎ ∈ 𝐻 ∧ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ) |
14 |
|
df-sh |
⊢ Sℋ = { ℎ ∈ 𝒫 ℋ ∣ ( 0ℎ ∈ ℎ ∧ ( +ℎ “ ( ℎ × ℎ ) ) ⊆ ℎ ∧ ( ·ℎ “ ( ℂ × ℎ ) ) ⊆ ℎ ) } |
15 |
13 14
|
elrab2 |
⊢ ( 𝐻 ∈ Sℋ ↔ ( 𝐻 ∈ 𝒫 ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ) |
16 |
|
anass |
⊢ ( ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ↔ ( 𝐻 ⊆ ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ) ) |
17 |
4 15 16
|
3bitr4i |
⊢ ( 𝐻 ∈ Sℋ ↔ ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ) |