Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gneispace Structured version   Visualization version   Unicode version
Theorem gneispace 38432
Description: The predicate that F is a (generic) Seifert And Threlfall neighborhood space. (Contributed by RP, 14-Apr-2021.)
Hypothesis
Ref Expression
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
Ref Expression
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 ) ) ) ) ) ) )
Distinct variable groups:   n, F, p, f   F, s, f   f, n, p   V, p
Allowed substitution hints:   A( f, n, s, p)   V( f, n, s)
Proof of Theorem gneispace
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 gneispace.a . . 3 |- 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 ) ) ) ) }
21gneispace3 38431 . 2 |- ( 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 790 . . . 4 |- ( ( ( 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 792 . . . . 5 |- ( ( ( 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 3737 . . . . . 6 |- ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) C_ ~P ( ~P dom F \ { (/) } )
6 difss 3737 . . . . . . 7 |- ( ~P dom F \ { (/) } ) C_ ~P dom F
7 sspwb 4917 . . . . . . 7 |- ( ( ~P dom F \ { (/) } ) C_ ~P dom F <-> ~P ( ~P dom F \ { (/) } ) C_ ~P ~P dom F )
86, 7mpbi 220 . . . . . 6 |- ~P ( ~P dom F \ { (/) } ) C_ ~P ~P dom F
95, 8sstri 3612 . . . . 5 |- ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) C_ ~P ~P dom F
104, 9syl6ss 3615 . . . 4 |- ( ( ( 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 )
11 simpr 477 . . . . . . 7 |- ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) -> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
12 simpl 473 . . . . . . . 8 |- ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) -> Fun F )
13 fvelrn 6352 . . . . . . . 8 |- ( ( Fun F /\ p e. dom F ) -> ( F ` p ) e. ran F )
1412, 13sylan 488 . . . . . . 7 |- ( ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) /\ p e. dom F ) -> ( F ` p ) e. ran F )
15 ssel2 3598 . . . . . . . 8 |- ( ( ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) /\ ( F ` p ) e. ran F ) -> ( F ` p ) e. ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) )
16 eldifsni 4320 . . . . . . . 8 |- ( ( F ` p ) e. ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) -> ( F ` p ) =/= (/) )
1715, 16syl 17 . . . . . . 7 |- ( ( ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) /\ ( F ` p ) e. ran F ) -> ( F ` p ) =/= (/) )
1811, 14, 17syl2an2r 876 . . . . . 6 |- ( ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) /\ p e. dom F ) -> ( F ` p ) =/= (/) )
1918ralrimiva 2966 . . . . 5 |- ( ( Fun F /\ ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) -> A. p e. dom F ( F ` p ) =/= (/) )
20 r19.26 3064 . . . . . 6 |- ( 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 ) ) ) ) )
2120biimpri 218 . . . . 5 |- ( ( 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 ) ) ) ) )
2219, 21sylan 488 . . . 4 |- ( ( ( 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 ) ) ) ) )
233, 10, 223jca 1242 . . 3 |- ( ( ( 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 ) ) ) ) ) )
24 simp1 1061 . . . . 5 |- ( ( 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 )
25 nfv 1843 . . . . . . . . . 10 |- F/ p Fun F
26 nfv 1843 . . . . . . . . . 10 |- F/ p ran F C_ ~P ~P dom F
27 nfra1 2941 . . . . . . . . . 10 |- 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 ) ) ) )
2825, 26, 27nf3an 1831 . . . . . . . . 9 |- 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 ) ) ) ) )
29 simpr 477 . . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) ) )
30 simpl 473 . . . . . . . . . . . . . . . . . 18 |- ( ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) -> p e. n )
31 19.8a 2052 . . . . . . . . . . . . . . . . . 18 |- ( p e. n -> E. p p e. n )
3230, 31syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( p e. n /\ A. s e. ~P dom F ( n C_ s -> s e. ( F ` p ) ) ) -> E. p p e. n )
3332ralimi 2952 . . . . . . . . . . . . . . . 16 |- ( 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 )
3429, 33syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( 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 )
3534ralimi 2952 . . . . . . . . . . . . . 14 |- ( 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 )
36353ad2ant3 1084 . . . . . . . . . . . . 13 |- ( ( 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 )
37 rsp 2929 . . . . . . . . . . . . 13 |- ( 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 ) )
3836, 37syl 17 . . . . . . . . . . . 12 |- ( ( 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 ) )
39 df-ex 1705 . . . . . . . . . . . . . . . . . . 19 |- ( E. p p e. n <-> -. A. p -. p e. n )
4039ralbii 2980 . . . . . . . . . . . . . . . . . 18 |- ( A. n e. ( F ` p ) E. p p e. n <-> A. n e. ( F ` p ) -. A. p -. p e. n )
41 ralnex 2992 . . . . . . . . . . . . . . . . . 18 |- ( A. n e. ( F ` p ) -. A. p -. p e. n <-> -. E. n e. ( F ` p ) A. p -. p e. n )
4240, 41bitri 264 . . . . . . . . . . . . . . . . 17 |- ( A. n e. ( F ` p ) E. p p e. n <-> -. E. n e. ( F ` p ) A. p -. p e. n )
43 0el 3939 . . . . . . . . . . . . . . . . 17 |- ( (/) e. ( F ` p ) <-> E. n e. ( F ` p ) A. p -. p e. n )
4442, 43xchbinxr 325 . . . . . . . . . . . . . . . 16 |- ( A. n e. ( F ` p ) E. p p e. n <-> -. (/) e. ( F ` p ) )
4544biimpi 206 . . . . . . . . . . . . . . 15 |- ( A. n e. ( F ` p ) E. p p e. n -> -. (/) e. ( F ` p ) )
46 elinel1 3799 . . . . . . . . . . . . . . 15 |- ( (/) e. ( ( F ` p ) i^i ~P dom F ) -> (/) e. ( F ` p ) )
4745, 46nsyl 135 . . . . . . . . . . . . . 14 |- ( A. n e. ( F ` p ) E. p p e. n -> -. (/) e. ( ( F ` p ) i^i ~P dom F ) )
48 disjsn 4246 . . . . . . . . . . . . . 14 |- ( ( ( ( F ` p ) i^i ~P dom F ) i^i { (/) } ) = (/) <-> -. (/) e. ( ( F ` p ) i^i ~P dom F ) )
4947, 48sylibr 224 . . . . . . . . . . . . 13 |- ( A. n e. ( F ` p ) E. p p e. n -> ( ( ( F ` p ) i^i ~P dom F ) i^i { (/) } ) = (/) )
50 disjdif2 4047 . . . . . . . . . . . . 13 |- ( ( ( ( F ` p ) i^i ~P dom F ) i^i { (/) } ) = (/) -> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( ( F ` p ) i^i ~P dom F ) )
5149, 50syl 17 . . . . . . . . . . . 12 |- ( A. n e. ( F ` p ) E. p p e. n -> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( ( F ` p ) i^i ~P dom F ) )
5238, 51syl6 35 . . . . . . . . . . 11 |- ( ( 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 ) ) )
53 simp2 1062 . . . . . . . . . . . 12 |- ( ( 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 )
5413ex 450 . . . . . . . . . . . . 13 |- ( Fun F -> ( p e. dom F -> ( F ` p ) e. ran F ) )
5524, 54syl 17 . . . . . . . . . . . 12 |- ( ( 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 ) )
56 ssel2 3598 . . . . . . . . . . . . 13 |- ( ( ran F C_ ~P ~P dom F /\ ( F ` p ) e. ran F ) -> ( F ` p ) e. ~P ~P dom F )
57 fvex 6201 . . . . . . . . . . . . . . 15 |- ( F ` p ) e. _V
5857elpw 4164 . . . . . . . . . . . . . 14 |- ( ( F ` p ) e. ~P ~P dom F <-> ( F ` p ) C_ ~P dom F )
59 df-ss 3588 . . . . . . . . . . . . . 14 |- ( ( F ` p ) C_ ~P dom F <-> ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) )
6058, 59sylbb 209 . . . . . . . . . . . . 13 |- ( ( F ` p ) e. ~P ~P dom F -> ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) )
6156, 60syl 17 . . . . . . . . . . . 12 |- ( ( ran F C_ ~P ~P dom F /\ ( F ` p ) e. ran F ) -> ( ( F ` p ) i^i ~P dom F ) = ( F ` p ) )
6253, 55, 61syl6an 568 . . . . . . . . . . 11 |- ( ( 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 ) ) )
6352, 62jcad 555 . . . . . . . . . 10 |- ( ( 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 ) ) ) )
64 eqtr 2641 . . . . . . . . . . 11 |- ( ( ( ( ( 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 ) )
65 df-ss 3588 . . . . . . . . . . . 12 |- ( ( F ` p ) C_ ( ~P dom F \ { (/) } ) <-> ( ( F ` p ) i^i ( ~P dom F \ { (/) } ) ) = ( F ` p ) )
66 indif2 3870 . . . . . . . . . . . . 13 |- ( ( F ` p ) i^i ( ~P dom F \ { (/) } ) ) = ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } )
6766eqeq1i 2627 . . . . . . . . . . . 12 |- ( ( ( F ` p ) i^i ( ~P dom F \ { (/) } ) ) = ( F ` p ) <-> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( F ` p ) )
6865, 67bitri 264 . . . . . . . . . . 11 |- ( ( F ` p ) C_ ( ~P dom F \ { (/) } ) <-> ( ( ( F ` p ) i^i ~P dom F ) \ { (/) } ) = ( F ` p ) )
6964, 68sylibr 224 . . . . . . . . . 10 |- ( ( ( ( ( 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 \ { (/) } ) )
7063, 69syl6 35 . . . . . . . . 9 |- ( ( 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 \ { (/) } ) ) )
7128, 70ralrimi 2957 . . . . . . . 8 |- ( ( 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 \ { (/) } ) )
72 funfn 5918 . . . . . . . . . . 11 |- ( Fun F <-> F Fn dom F )
7372biimpi 206 . . . . . . . . . 10 |- ( Fun F -> F Fn dom F )
7424, 73syl 17 . . . . . . . . 9 |- ( ( 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 )
75 sseq1 3626 . . . . . . . . . 10 |- ( x = ( F ` p ) -> ( x C_ ( ~P dom F \ { (/) } ) <-> ( F ` p ) C_ ( ~P dom F \ { (/) } ) ) )
7675ralrn 6362 . . . . . . . . 9 |- ( 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 \ { (/) } ) ) )
7774, 76syl 17 . . . . . . . 8 |- ( ( 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 \ { (/) } ) ) )
7871, 77mpbird 247 . . . . . . 7 |- ( ( 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 \ { (/) } ) )
79 pwssb 4612 . . . . . . 7 |- ( ran F C_ ~P ( ~P dom F \ { (/) } ) <-> A. x e. ran F x C_ ( ~P dom F \ { (/) } ) )
8078, 79sylibr 224 . . . . . 6 |- ( ( 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 \ { (/) } ) )
81 simpl 473 . . . . . . . . . 10 |- ( ( ( 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 ) =/= (/) )
8281ralimi 2952 . . . . . . . . 9 |- ( 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 ) =/= (/) )
83823ad2ant3 1084 . . . . . . . 8 |- ( ( 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 ) =/= (/) )
8424, 83jca 554 . . . . . . 7 |- ( ( 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 ) =/= (/) ) )
85 elrnrexdm 6363 . . . . . . . . . 10 |- ( Fun F -> ( (/) e. ran F -> E. p e. dom F (/) = ( F ` p ) ) )
86 nesym 2850 . . . . . . . . . . . 12 |- ( ( F ` p ) =/= (/) <-> -. (/) = ( F ` p ) )
8786ralbii 2980 . . . . . . . . . . 11 |- ( A. p e. dom F ( F ` p ) =/= (/) <-> A. p e. dom F -. (/) = ( F ` p ) )
88 ralnex 2992 . . . . . . . . . . 11 |- ( A. p e. dom F -. (/) = ( F ` p ) <-> -. E. p e. dom F (/) = ( F ` p ) )
8987, 88sylbb 209 . . . . . . . . . 10 |- ( A. p e. dom F ( F ` p ) =/= (/) -> -. E. p e. dom F (/) = ( F ` p ) )
9085, 89nsyli 155 . . . . . . . . 9 |- ( Fun F -> ( A. p e. dom F ( F ` p ) =/= (/) -> -. (/) e. ran F ) )
9190imp 445 . . . . . . . 8 |- ( ( Fun F /\ A. p e. dom F ( F ` p ) =/= (/) ) -> -. (/) e. ran F )
92 disjsn 4246 . . . . . . . 8 |- ( ( ran F i^i { (/) } ) = (/) <-> -. (/) e. ran F )
9391, 92sylibr 224 . . . . . . 7 |- ( ( Fun F /\ A. p e. dom F ( F ` p ) =/= (/) ) -> ( ran F i^i { (/) } ) = (/) )
9484, 93syl 17 . . . . . 6 |- ( ( 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 { (/) } ) = (/) )
95 reldisj 4020 . . . . . . 7 |- ( ran F C_ ~P ( ~P dom F \ { (/) } ) -> ( ( ran F i^i { (/) } ) = (/) <-> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
9695biimpd 219 . . . . . 6 |- ( ran F C_ ~P ( ~P dom F \ { (/) } ) -> ( ( ran F i^i { (/) } ) = (/) -> ran F C_ ( ~P ( ~P dom F \ { (/) } ) \ { (/) } ) ) )
9780, 94, 96sylc 65 . . . . 5 |- ( ( 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 \ { (/) } ) \ { (/) } ) )
9824, 97jca 554 . . . 4 |- ( ( 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 \ { (/) } ) \ { (/) } ) ) )
9920biimpi 206 . . . . . 6 |- ( 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 ) ) ) ) )
100993ad2ant3 1084 . . . . 5 |- ( ( 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 ) ) ) ) )
101 simpr 477 . . . . 5 |- ( ( 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 ) ) ) )
102100, 101syl 17 . . . 4 |- ( ( 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 ) ) ) )
10398, 102jca 554 . . 3 |- ( ( 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 ) ) ) ) )
10423, 103impbii 199 . 2 |- ( ( ( 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 ) ) ) ) ) )
1052, 104syl6bb 276 1 |- ( 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 ) ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   \ cdif 3571   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   dom cdm 5114   ran crn 5115   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896
This theorem is referenced by:  gneispacef2  38434  gneispacern2  38437  gneispace0nelrn  38438
  Copyright terms: Public domain W3C validator