Step |
Hyp |
Ref |
Expression |
1 |
|
ssid |
|- ~H C_ ~H |
2 |
|
ax-hv0cl |
|- 0h e. ~H |
3 |
1 2
|
pm3.2i |
|- ( ~H C_ ~H /\ 0h e. ~H ) |
4 |
|
hvaddcl |
|- ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) e. ~H ) |
5 |
4
|
rgen2 |
|- A. x e. ~H A. y e. ~H ( x +h y ) e. ~H |
6 |
|
hvmulcl |
|- ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H ) |
7 |
6
|
rgen2 |
|- A. x e. CC A. y e. ~H ( x .h y ) e. ~H |
8 |
5 7
|
pm3.2i |
|- ( A. x e. ~H A. y e. ~H ( x +h y ) e. ~H /\ A. x e. CC A. y e. ~H ( x .h y ) e. ~H ) |
9 |
|
issh2 |
|- ( ~H e. SH <-> ( ( ~H C_ ~H /\ 0h e. ~H ) /\ ( A. x e. ~H A. y e. ~H ( x +h y ) e. ~H /\ A. x e. CC A. y e. ~H ( x .h y ) e. ~H ) ) ) |
10 |
3 8 9
|
mpbir2an |
|- ~H e. SH |
11 |
|
vex |
|- x e. _V |
12 |
11
|
hlimveci |
|- ( f ~~>v x -> x e. ~H ) |
13 |
12
|
adantl |
|- ( ( f : NN --> ~H /\ f ~~>v x ) -> x e. ~H ) |
14 |
13
|
gen2 |
|- A. f A. x ( ( f : NN --> ~H /\ f ~~>v x ) -> x e. ~H ) |
15 |
|
isch2 |
|- ( ~H e. CH <-> ( ~H e. SH /\ A. f A. x ( ( f : NN --> ~H /\ f ~~>v x ) -> x e. ~H ) ) ) |
16 |
10 14 15
|
mpbir2an |
|- ~H e. CH |