Step |
Hyp |
Ref |
Expression |
1 |
|
isnrm |
|- ( J e. Nrm <-> ( J e. Top /\ A. y e. J A. z e. ( ( Clsd ` J ) i^i ~P y ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) ) ) |
2 |
|
pweq |
|- ( y = A -> ~P y = ~P A ) |
3 |
2
|
ineq2d |
|- ( y = A -> ( ( Clsd ` J ) i^i ~P y ) = ( ( Clsd ` J ) i^i ~P A ) ) |
4 |
|
sseq2 |
|- ( y = A -> ( ( ( cls ` J ) ` x ) C_ y <-> ( ( cls ` J ) ` x ) C_ A ) ) |
5 |
4
|
anbi2d |
|- ( y = A -> ( ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) <-> ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
6 |
5
|
rexbidv |
|- ( y = A -> ( E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) <-> E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
7 |
3 6
|
raleqbidv |
|- ( y = A -> ( A. z e. ( ( Clsd ` J ) i^i ~P y ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) <-> A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
8 |
7
|
rspccv |
|- ( A. y e. J A. z e. ( ( Clsd ` J ) i^i ~P y ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ y ) -> ( A e. J -> A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
9 |
1 8
|
simplbiim |
|- ( J e. Nrm -> ( A e. J -> A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
10 |
|
elin |
|- ( B e. ( ( Clsd ` J ) i^i ~P A ) <-> ( B e. ( Clsd ` J ) /\ B e. ~P A ) ) |
11 |
|
elpwg |
|- ( B e. ( Clsd ` J ) -> ( B e. ~P A <-> B C_ A ) ) |
12 |
11
|
pm5.32i |
|- ( ( B e. ( Clsd ` J ) /\ B e. ~P A ) <-> ( B e. ( Clsd ` J ) /\ B C_ A ) ) |
13 |
10 12
|
bitri |
|- ( B e. ( ( Clsd ` J ) i^i ~P A ) <-> ( B e. ( Clsd ` J ) /\ B C_ A ) ) |
14 |
|
cleq1lem |
|- ( z = B -> ( ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) <-> ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
15 |
14
|
rexbidv |
|- ( z = B -> ( E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) <-> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
16 |
15
|
rspccv |
|- ( A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) -> ( B e. ( ( Clsd ` J ) i^i ~P A ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
17 |
13 16
|
syl5bir |
|- ( A. z e. ( ( Clsd ` J ) i^i ~P A ) E. x e. J ( z C_ x /\ ( ( cls ` J ) ` x ) C_ A ) -> ( ( B e. ( Clsd ` J ) /\ B C_ A ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) |
18 |
9 17
|
syl6 |
|- ( J e. Nrm -> ( A e. J -> ( ( B e. ( Clsd ` J ) /\ B C_ A ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) ) |
19 |
18
|
exp4a |
|- ( J e. Nrm -> ( A e. J -> ( B e. ( Clsd ` J ) -> ( B C_ A -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) ) ) ) |
20 |
19
|
3imp2 |
|- ( ( J e. Nrm /\ ( A e. J /\ B e. ( Clsd ` J ) /\ B C_ A ) ) -> E. x e. J ( B C_ x /\ ( ( cls ` J ) ` x ) C_ A ) ) |