Metamath Proof Explorer


Theorem gneispace

Description: The predicate that F is a (generic) Seifert and Threlfall neighborhood space. (Contributed by RP, 14-Apr-2021)

Ref Expression
Hypothesis 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 ) ) ) ) }
Assertion gneispace
|- ( F e. V -> ( F e. A <-> ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) ) )

Proof

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 gneispace3
 |-  ( F e. V -> ( F e. A <-> ( ( Fun F /\ ran F C_ ( ~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 simpll
 |-  ( ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) -> Fun F )
4 simplr
 |-  ( ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) -> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
5 difss
 |-  ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) C_ ~P ( ~P dom F \ { (/) } )
6 difss
 |-  ( ~P dom F \ { (/) } ) C_ ~P dom F
7 6 sspwi
 |-  ~P ( ~P dom F \ { (/) } ) C_ ~P ~P dom F
8 5 7 sstri
 |-  ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) C_ ~P ~P dom F
9 4 8 sstrdi
 |-  ( ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) -> ran F C_ ~P ~P dom F )
10 simpr
 |-  ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) -> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
11 simpl
 |-  ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) -> Fun F )
12 fvelrn
 |-  ( ( Fun F /\ p e. dom F ) -> ( F ` p ) e. ran F )
13 11 12 sylan
 |-  ( ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) /\ p e. dom F ) -> ( F ` p ) e. ran F )
14 ssel2
 |-  ( ( ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) /\ ( F ` p ) e. ran F ) -> ( F ` p ) e. ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
15 eldifsni
 |-  ( ( F ` p ) e. ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) -> ( F ` p ) =/= (/) )
16 14 15 syl
 |-  ( ( ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) /\ ( F ` p ) e. ran F ) -> ( F ` p ) =/= (/) )
17 10 13 16 syl2an2r
 |-  ( ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) /\ p e. dom F ) -> ( F ` p ) =/= (/) )
18 17 ralrimiva
 |-  ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) -> A. p e. dom F ( F ` p ) =/= (/) )
19 r19.26
 |-  ( A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 ( F ` p ) =/= (/) /\ 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 ) ) ) ) )
20 19 biimpri
 |-  ( ( A. p e. dom F ( F ` p ) =/= (/) /\ 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 ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) )
21 18 20 sylan
 |-  ( ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) -> A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) )
22 3 9 21 3jca
 |-  ( ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) -> ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) )
23 simp1
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> Fun F )
24 nfv
 |-  F/ p Fun F
25 nfv
 |-  F/ p ran F C_ ~P ~P dom F
26 nfra1
 |-  F/ p A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) )
27 24 25 26 nf3an
 |-  F/ p ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) )
28 simpr
 |-  ( ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) -> A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) )
29 simpl
 |-  ( ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) -> p e. n )
30 29 19.8ad
 |-  ( ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) -> E. p p e. n )
31 30 ralimi
 |-  ( A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) -> A. n e. ( F ` p ) E. p p e. n )
32 28 31 syl
 |-  ( ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) -> A. n e. ( F ` p ) E. p p e. n )
33 32 ralimi
 |-  ( A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 ) E. p p e. n )
34 33 3ad2ant3
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 ) E. p p e. n )
35 rsp
 |-  ( A. p e. dom F A. n e. ( F ` p ) E. p p e. n -> ( p e. dom F -> A. n e. ( F ` p ) E. p p e. n ) )
36 34 35 syl
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( p e. dom F -> A. n e. ( F ` p ) E. p p e. n ) )
37 df-ex
 |-  ( E. p p e. n <-> -. A. p -. p e. n )
38 37 ralbii
 |-  ( A. n e. ( F ` p ) E. p p e. n <-> A. n e. ( F ` p ) -. A. p -. p e. n )
39 ralnex
 |-  ( A. n e. ( F ` p ) -. A. p -. p e. n <-> -. E. n e. ( F ` p ) A. p -. p e. n )
40 38 39 bitri
 |-  ( A. n e. ( F ` p ) E. p p e. n <-> -. E. n e. ( F ` p ) A. p -. p e. n )
41 0el
 |-  ( (/) e. ( F ` p ) <-> E. n e. ( F ` p ) A. p -. p e. n )
42 40 41 xchbinxr
 |-  ( A. n e. ( F ` p ) E. p p e. n <-> -. (/) e. ( F ` p ) )
43 42 biimpi
 |-  ( A. n e. ( F ` p ) E. p p e. n -> -. (/) e. ( F ` p ) )
44 elinel1
 |-  ( (/) e. ( ( F ` p ) i^i ~P dom F ) -> (/) e. ( F ` p ) )
45 43 44 nsyl
 |-  ( A. n e. ( F ` p ) E. p p e. n -> -. (/) e. ( ( F ` p ) i^i ~P dom F ) )
46 disjsn
 |-  ( ( ( ( F ` p ) i^i ~P dom F ) i^i { (/) } ) = (/) <-> -. (/) e. ( ( F ` p ) i^i ~P dom F ) )
47 45 46 sylibr
 |-  ( A. n e. ( F ` p ) E. p p e. n -> ( ( ( F ` p ) i^i ~P dom F ) i^i { (/) } ) = (/) )
48 disjdif2
 |-  ( ( ( ( F ` p ) i^i ~P dom F ) i^i { (/) } ) = (/) -> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( ( F ` p ) i^i ~P dom F ) )
49 47 48 syl
 |-  ( A. n e. ( F ` p ) E. p p e. n -> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( ( F ` p ) i^i ~P dom F ) )
50 36 49 syl6
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( p e. dom F -> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( ( F ` p ) i^i ~P dom F ) ) )
51 simp2
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ran F C_ ~P ~P dom F )
52 12 ex
 |-  ( Fun F -> ( p e. dom F -> ( F ` p ) e. ran F ) )
53 23 52 syl
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( p e. dom F -> ( F ` p ) e. ran F ) )
54 ssel2
 |-  ( ( ran F C_ ~P ~P dom F /\ ( F ` p ) e. ran F ) -> ( F ` p ) e. ~P ~P dom F )
55 fvex
 |-  ( F ` p ) e. _V
56 55 elpw
 |-  ( ( F ` p ) e. ~P ~P dom F <-> ( F ` p ) C_ ~P dom F )
57 df-ss
 |-  ( ( F ` p ) C_ ~P dom F <-> ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) )
58 56 57 sylbb
 |-  ( ( F ` p ) e. ~P ~P dom F -> ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) )
59 54 58 syl
 |-  ( ( ran F C_ ~P ~P dom F /\ ( F ` p ) e. ran F ) -> ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) )
60 51 53 59 syl6an
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( p e. dom F -> ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) ) )
61 50 60 jcad
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( p e. dom F -> ( ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( ( F ` p ) i^i ~P dom F ) /\ ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) ) ) )
62 eqtr
 |-  ( ( ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( ( F ` p ) i^i ~P dom F ) /\ ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) ) -> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( F ` p ) )
63 df-ss
 |-  ( ( F ` p ) C_ ( ~P dom F \ { (/) } ) <-> ( ( F ` p ) i^i ( ~P dom F \ { (/) } ) ) = ( F ` p ) )
64 indif2
 |-  ( ( F ` p ) i^i ( ~P dom F \ { (/) } ) ) = ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } )
65 64 eqeq1i
 |-  ( ( ( F ` p ) i^i ( ~P dom F \ { (/) } ) ) = ( F ` p ) <-> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( F ` p ) )
66 63 65 bitri
 |-  ( ( F ` p ) C_ ( ~P dom F \ { (/) } ) <-> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( F ` p ) )
67 62 66 sylibr
 |-  ( ( ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( ( F ` p ) i^i ~P dom F ) /\ ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) ) -> ( F ` p ) C_ ( ~P dom F \ { (/) } ) )
68 61 67 syl6
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( p e. dom F -> ( F ` p ) C_ ( ~P dom F \ { (/) } ) ) )
69 27 68 ralrimi
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 ( F ` p ) C_ ( ~P dom F \ { (/) } ) )
70 23 funfnd
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> F Fn dom F )
71 sseq1
 |-  ( x = ( F ` p ) -> ( x C_ ( ~P dom F \ { (/) } ) <-> ( F ` p ) C_ ( ~P dom F \ { (/) } ) ) )
72 71 ralrn
 |-  ( F Fn dom F -> ( A. x e. ran F x C_ ( ~P dom F \ { (/) } ) <-> A. p e. dom F ( F ` p ) C_ ( ~P dom F \ { (/) } ) ) )
73 70 72 syl
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( A. x e. ran F x C_ ( ~P dom F \ { (/) } ) <-> A. p e. dom F ( F ` p ) C_ ( ~P dom F \ { (/) } ) ) )
74 69 73 mpbird
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> A. x e. ran F x C_ ( ~P dom F \ { (/) } ) )
75 pwssb
 |-  ( ran F C_ ~P ( ~P dom F \ { (/) } ) <-> A. x e. ran F x C_ ( ~P dom F \ { (/) } ) )
76 74 75 sylibr
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ran F C_ ~P ( ~P dom F \ { (/) } ) )
77 simpl
 |-  ( ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) -> ( F ` p ) =/= (/) )
78 77 ralimi
 |-  ( A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 ( F ` p ) =/= (/) )
79 78 3ad2ant3
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 ( F ` p ) =/= (/) )
80 23 79 jca
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( Fun F /\ A. p e. dom F ( F ` p ) =/= (/) ) )
81 elrnrexdm
 |-  ( Fun F -> ( (/) e. ran F -> E. p e. dom F (/) = ( F ` p ) ) )
82 nesym
 |-  ( ( F ` p ) =/= (/) <-> -. (/) = ( F ` p ) )
83 82 ralbii
 |-  ( A. p e. dom F ( F ` p ) =/= (/) <-> A. p e. dom F -. (/) = ( F ` p ) )
84 ralnex
 |-  ( A. p e. dom F -. (/) = ( F ` p ) <-> -. E. p e. dom F (/) = ( F ` p ) )
85 83 84 sylbb
 |-  ( A. p e. dom F ( F ` p ) =/= (/) -> -. E. p e. dom F (/) = ( F ` p ) )
86 81 85 nsyli
 |-  ( Fun F -> ( A. p e. dom F ( F ` p ) =/= (/) -> -. (/) e. ran F ) )
87 86 imp
 |-  ( ( Fun F /\ A. p e. dom F ( F ` p ) =/= (/) ) -> -. (/) e. ran F )
88 disjsn
 |-  ( ( ran F i^i { (/) } ) = (/) <-> -. (/) e. ran F )
89 87 88 sylibr
 |-  ( ( Fun F /\ A. p e. dom F ( F ` p ) =/= (/) ) -> ( ran F i^i { (/) } ) = (/) )
90 80 89 syl
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( ran F i^i { (/) } ) = (/) )
91 reldisj
 |-  ( ran F C_ ~P ( ~P dom F \ { (/) } ) -> ( ( ran F i^i { (/) } ) = (/) <-> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
92 91 biimpd
 |-  ( ran F C_ ~P ( ~P dom F \ { (/) } ) -> ( ( ran F i^i { (/) } ) = (/) -> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
93 76 90 92 sylc
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
94 23 93 jca
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
95 19 biimpi
 |-  ( A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 ( F ` p ) =/= (/) /\ 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 ) ) ) ) )
96 95 3ad2ant3
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 ( F ` p ) =/= (/) /\ 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 ) ) ) ) )
97 simpr
 |-  ( ( A. p e. dom F ( F ` p ) =/= (/) /\ 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 /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) )
98 96 97 syl
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ 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 /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) )
99 94 98 jca
 |-  ( ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) -> ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) )
100 22 99 impbii
 |-  ( ( ( Fun F /\ ran F C_ ( ~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 ) ) ) ) <-> ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) )
101 2 100 bitrdi
 |-  ( F e. V -> ( F e. A <-> ( Fun F /\ ran F C_ ~P ~P dom F /\ A. p e. dom F ( ( F ` p ) =/= (/) /\ A. n e. ( F ` p ) ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) ) ) ) )