Step |
Hyp |
Ref |
Expression |
1 |
|
gneispace.a |
|- A = { f | ( f : dom f --> ( ~P ( ~P dom f \ { (/) } ) \ { (/) } ) /\ A. p e. dom f A. n e. ( f ` p ) ( p e. n /\ A. s e. ~P dom f ( n C_ s -> s e. ( f ` p ) ) ) ) } |
2 |
1
|
gneispace2 |
|- ( F e. A -> ( F e. A <-> ( F : dom F --> ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) /\ A. p e. dom F A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) ) |
3 |
2
|
ibi |
|- ( F e. A -> ( F : dom F --> ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) /\ A. p e. dom F A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) |
4 |
|
simpl |
|- ( ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) -> p e. n ) |
5 |
4
|
2ralimi |
|- ( A. p e. dom F A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) -> A. p e. dom F A. n e. ( F ` p ) p e. n ) |
6 |
3 5
|
simpl2im |
|- ( F e. A -> A. p e. dom F A. n e. ( F ` p ) p e. n ) |