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 dfss2 
 |-  ( ( 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 dfss2 
 |-  ( ( 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 ) ) ) ) ) ) )