Metamath Proof Explorer

Theorem fvineqsneq

Description: A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 28-Mar-2021)

Ref Expression
Assertion fvineqsneq 
|- ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( Z C_ ran F /\ A C_ U. Z ) ) -> Z = ran F )

Proof

Step Hyp Ref Expression
1 pssnel 
 |-  ( Z C. ran F -> E. x ( x e. ran F /\ -. x e. Z ) )
2 1 adantl 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. x ( x e. ran F /\ -. x e. Z ) )
3 df-rex 
 |-  ( E. x e. ran F -. x e. Z <-> E. x ( x e. ran F /\ -. x e. Z ) )
4 2 3 sylibr 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. x e. ran F -. x e. Z )
5 fnrnfv 
 |-  ( F Fn A -> ran F = { x | E. p e. A x = ( F ` p ) } )
6 5 eqabrd 
 |-  ( F Fn A -> ( x e. ran F <-> E. p e. A x = ( F ` p ) ) )
7 6 biimpd 
 |-  ( F Fn A -> ( x e. ran F -> E. p e. A x = ( F ` p ) ) )
8 7 ralrimiv 
 |-  ( F Fn A -> A. x e. ran F E. p e. A x = ( F ` p ) )
9 8 adantr 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> A. x e. ran F E. p e. A x = ( F ` p ) )
10 9 adantr 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> A. x e. ran F E. p e. A x = ( F ` p ) )
11 r19.29r 
 |-  ( ( E. x e. ran F -. x e. Z /\ A. x e. ran F E. p e. A x = ( F ` p ) ) -> E. x e. ran F ( -. x e. Z /\ E. p e. A x = ( F ` p ) ) )
12 4 10 11 syl2anc 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. x e. ran F ( -. x e. Z /\ E. p e. A x = ( F ` p ) ) )
13 nfra1 
 |-  F/ p A. p e. A ( ( F ` p ) i^i A ) = { p }
14 rsp 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> ( p e. A -> ( ( F ` p ) i^i A ) = { p } ) )
15 vsnid 
 |-  p e. { p }
16 eleq2 
 |-  ( ( ( F ` p ) i^i A ) = { p } -> ( p e. ( ( F ` p ) i^i A ) <-> p e. { p } ) )
17 15 16 mpbiri 
 |-  ( ( ( F ` p ) i^i A ) = { p } -> p e. ( ( F ` p ) i^i A ) )
18 17 elin1d 
 |-  ( ( ( F ` p ) i^i A ) = { p } -> p e. ( F ` p ) )
19 14 18 syl6 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> ( p e. A -> p e. ( F ` p ) ) )
20 19 adantr 
 |-  ( ( A. p e. A ( ( F ` p ) i^i A ) = { p } /\ x = ( F ` p ) ) -> ( p e. A -> p e. ( F ` p ) ) )
21 eleq2 
 |-  ( x = ( F ` p ) -> ( p e. x <-> p e. ( F ` p ) ) )
22 21 adantl 
 |-  ( ( A. p e. A ( ( F ` p ) i^i A ) = { p } /\ x = ( F ` p ) ) -> ( p e. x <-> p e. ( F ` p ) ) )
23 20 22 sylibrd 
 |-  ( ( A. p e. A ( ( F ` p ) i^i A ) = { p } /\ x = ( F ` p ) ) -> ( p e. A -> p e. x ) )
24 23 ex 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> ( x = ( F ` p ) -> ( p e. A -> p e. x ) ) )
25 24 com23 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> ( p e. A -> ( x = ( F ` p ) -> p e. x ) ) )
26 13 25 reximdai 
 |-  ( A. p e. A ( ( F ` p ) i^i A ) = { p } -> ( E. p e. A x = ( F ` p ) -> E. p e. A p e. x ) )
27 26 adantl 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( E. p e. A x = ( F ` p ) -> E. p e. A p e. x ) )
28 27 adantr 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( E. p e. A x = ( F ` p ) -> E. p e. A p e. x ) )
29 28 anim2d 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( ( -. x e. Z /\ E. p e. A x = ( F ` p ) ) -> ( -. x e. Z /\ E. p e. A p e. x ) ) )
30 29 reximdv 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( E. x e. ran F ( -. x e. Z /\ E. p e. A x = ( F ` p ) ) -> E. x e. ran F ( -. x e. Z /\ E. p e. A p e. x ) ) )
31 12 30 mpd 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. x e. ran F ( -. x e. Z /\ E. p e. A p e. x ) )
32 ancom 
 |-  ( ( -. x e. Z /\ E. p e. A p e. x ) <-> ( E. p e. A p e. x /\ -. x e. Z ) )
33 r19.41v 
 |-  ( E. p e. A ( p e. x /\ -. x e. Z ) <-> ( E. p e. A p e. x /\ -. x e. Z ) )
34 32 33 bitr4i 
 |-  ( ( -. x e. Z /\ E. p e. A p e. x ) <-> E. p e. A ( p e. x /\ -. x e. Z ) )
35 34 rexbii 
 |-  ( E. x e. ran F ( -. x e. Z /\ E. p e. A p e. x ) <-> E. x e. ran F E. p e. A ( p e. x /\ -. x e. Z ) )
36 31 35 sylib 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. x e. ran F E. p e. A ( p e. x /\ -. x e. Z ) )
37 rexcom 
 |-  ( E. p e. A E. x e. ran F ( p e. x /\ -. x e. Z ) <-> E. x e. ran F E. p e. A ( p e. x /\ -. x e. Z ) )
38 36 37 sylibr 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. p e. A E. x e. ran F ( p e. x /\ -. x e. Z ) )
39 nfre1 
 |-  F/ x E. x e. ran F ( p e. x /\ -. x e. Z )
40 39 19.3 
 |-  ( A. x E. x e. ran F ( p e. x /\ -. x e. Z ) <-> E. x e. ran F ( p e. x /\ -. x e. Z ) )
41 alral 
 |-  ( A. x E. x e. ran F ( p e. x /\ -. x e. Z ) -> A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) )
42 40 41 sylbir 
 |-  ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) )
43 42 reximi 
 |-  ( E. p e. A E. x e. ran F ( p e. x /\ -. x e. Z ) -> E. p e. A A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) )
44 38 43 syl 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. p e. A A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) )
45 nfv 
 |-  F/ p F Fn A
46 45 13 nfan 
 |-  F/ p ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } )
47 nfv 
 |-  F/ p Z C. ran F
48 46 47 nfan 
 |-  F/ p ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F )
49 nfv 
 |-  F/ x ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ p e. A )
50 fvineqsneu 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> A. p e. A E! x e. ran F p e. x )
51 50 adantr 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> A. p e. A E! x e. ran F p e. x )
52 rsp 
 |-  ( A. p e. A E! x e. ran F p e. x -> ( p e. A -> E! x e. ran F p e. x ) )
53 51 52 syl 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( p e. A -> E! x e. ran F p e. x ) )
54 53 adantrd 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( ( p e. A /\ x e. ran F ) -> E! x e. ran F p e. x ) )
55 54 imp 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ ( p e. A /\ x e. ran F ) ) -> E! x e. ran F p e. x )
56 reupick3 
 |-  ( ( E! x e. ran F p e. x /\ E. x e. ran F ( p e. x /\ -. x e. Z ) /\ x e. ran F ) -> ( p e. x -> -. x e. Z ) )
57 56 3expa 
 |-  ( ( ( E! x e. ran F p e. x /\ E. x e. ran F ( p e. x /\ -. x e. Z ) ) /\ x e. ran F ) -> ( p e. x -> -. x e. Z ) )
58 57 expcom 
 |-  ( x e. ran F -> ( ( E! x e. ran F p e. x /\ E. x e. ran F ( p e. x /\ -. x e. Z ) ) -> ( p e. x -> -. x e. Z ) ) )
59 58 adantl 
 |-  ( ( p e. A /\ x e. ran F ) -> ( ( E! x e. ran F p e. x /\ E. x e. ran F ( p e. x /\ -. x e. Z ) ) -> ( p e. x -> -. x e. Z ) ) )
60 59 adantl 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ ( p e. A /\ x e. ran F ) ) -> ( ( E! x e. ran F p e. x /\ E. x e. ran F ( p e. x /\ -. x e. Z ) ) -> ( p e. x -> -. x e. Z ) ) )
61 55 60 mpand 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ ( p e. A /\ x e. ran F ) ) -> ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) )
62 61 expr 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ p e. A ) -> ( x e. ran F -> ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) ) )
63 49 62 ralrimi 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ p e. A ) -> A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) )
64 63 ex 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( p e. A -> A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) ) )
65 48 64 ralrimi 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> A. p e. A A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) )
66 r19.29r 
 |-  ( ( E. p e. A A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) /\ A. p e. A A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) ) -> E. p e. A ( A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) /\ A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) ) )
67 44 65 66 syl2anc 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. p e. A ( A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) /\ A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) ) )
68 ralim 
 |-  ( A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) -> ( A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) -> A. x e. ran F ( p e. x -> -. x e. Z ) ) )
69 68 impcom 
 |-  ( ( A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) /\ A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) ) -> A. x e. ran F ( p e. x -> -. x e. Z ) )
70 69 reximi 
 |-  ( E. p e. A ( A. x e. ran F E. x e. ran F ( p e. x /\ -. x e. Z ) /\ A. x e. ran F ( E. x e. ran F ( p e. x /\ -. x e. Z ) -> ( p e. x -> -. x e. Z ) ) ) -> E. p e. A A. x e. ran F ( p e. x -> -. x e. Z ) )
71 67 70 syl 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. p e. A A. x e. ran F ( p e. x -> -. x e. Z ) )
72 con2b 
 |-  ( ( p e. x -> -. x e. Z ) <-> ( x e. Z -> -. p e. x ) )
73 72 ralbii 
 |-  ( A. x e. ran F ( p e. x -> -. x e. Z ) <-> A. x e. ran F ( x e. Z -> -. p e. x ) )
74 df-ral 
 |-  ( A. x e. ran F ( x e. Z -> -. p e. x ) <-> A. x ( x e. ran F -> ( x e. Z -> -. p e. x ) ) )
75 bi2.04 
 |-  ( ( x e. ran F -> ( x e. Z -> -. p e. x ) ) <-> ( x e. Z -> ( x e. ran F -> -. p e. x ) ) )
76 75 albii 
 |-  ( A. x ( x e. ran F -> ( x e. Z -> -. p e. x ) ) <-> A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) )
77 73 74 76 3bitri 
 |-  ( A. x e. ran F ( p e. x -> -. x e. Z ) <-> A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) )
78 77 a1i 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( A. x e. ran F ( p e. x -> -. x e. Z ) <-> A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) ) )
79 48 78 rexbid 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( E. p e. A A. x e. ran F ( p e. x -> -. x e. Z ) <-> E. p e. A A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) ) )
80 71 79 mpbid 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. p e. A A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) )
81 nfv 
 |-  F/ x ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F )
82 nfa1 
 |-  F/ x A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) )
83 81 82 nfan 
 |-  F/ x ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) )
84 pssss 
 |-  ( Z C. ran F -> Z C_ ran F )
85 df-ss 
 |-  ( Z C_ ran F <-> A. x ( x e. Z -> x e. ran F ) )
86 84 85 sylib 
 |-  ( Z C. ran F -> A. x ( x e. Z -> x e. ran F ) )
87 86 adantl 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> A. x ( x e. Z -> x e. ran F ) )
88 df-ral 
 |-  ( A. x e. Z x e. ran F <-> A. x ( x e. Z -> x e. ran F ) )
89 87 88 sylibr 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> A. x e. Z x e. ran F )
90 89 adantr 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) ) -> A. x e. Z x e. ran F )
91 rsp 
 |-  ( A. x e. Z x e. ran F -> ( x e. Z -> x e. ran F ) )
92 90 91 syl 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) ) -> ( x e. Z -> x e. ran F ) )
93 df-ral 
 |-  ( A. x e. Z ( x e. ran F -> -. p e. x ) <-> A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) )
94 93 biimpri 
 |-  ( A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) -> A. x e. Z ( x e. ran F -> -. p e. x ) )
95 94 adantl 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) ) -> A. x e. Z ( x e. ran F -> -. p e. x ) )
96 rsp 
 |-  ( A. x e. Z ( x e. ran F -> -. p e. x ) -> ( x e. Z -> ( x e. ran F -> -. p e. x ) ) )
97 95 96 syl 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) ) -> ( x e. Z -> ( x e. ran F -> -. p e. x ) ) )
98 92 97 mpdd 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) ) -> ( x e. Z -> -. p e. x ) )
99 83 98 ralrimi 
 |-  ( ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) /\ A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) ) -> A. x e. Z -. p e. x )
100 99 ex 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) -> A. x e. Z -. p e. x ) )
101 100 a1d 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( p e. A -> ( A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) -> A. x e. Z -. p e. x ) ) )
102 48 101 reximdai 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> ( E. p e. A A. x ( x e. Z -> ( x e. ran F -> -. p e. x ) ) -> E. p e. A A. x e. Z -. p e. x ) )
103 80 102 mpd 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. p e. A A. x e. Z -. p e. x )
104 ralnex 
 |-  ( A. x e. Z -. p e. x <-> -. E. x e. Z p e. x )
105 104 rexbii 
 |-  ( E. p e. A A. x e. Z -. p e. x <-> E. p e. A -. E. x e. Z p e. x )
106 103 105 sylib 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. p e. A -. E. x e. Z p e. x )
107 eluni2 
 |-  ( p e. U. Z <-> E. x e. Z p e. x )
108 107 notbii 
 |-  ( -. p e. U. Z <-> -. E. x e. Z p e. x )
109 108 rexbii 
 |-  ( E. p e. A -. p e. U. Z <-> E. p e. A -. E. x e. Z p e. x )
110 106 109 sylibr 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> E. p e. A -. p e. U. Z )
111 dfss3 
 |-  ( A C_ U. Z <-> A. p e. A p e. U. Z )
112 dfral2 
 |-  ( A. p e. A p e. U. Z <-> -. E. p e. A -. p e. U. Z )
113 111 112 bitri 
 |-  ( A C_ U. Z <-> -. E. p e. A -. p e. U. Z )
114 113 con2bii2 
 |-  ( -. A C_ U. Z <-> E. p e. A -. p e. U. Z )
115 110 114 sylibr 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ Z C. ran F ) -> -. A C_ U. Z )
116 115 ex 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( Z C. ran F -> -. A C_ U. Z ) )
117 116 con2d 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( A C_ U. Z -> -. Z C. ran F ) )
118 npss 
 |-  ( -. Z C. ran F <-> ( Z C_ ran F -> Z = ran F ) )
119 117 118 imbitrdi 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( A C_ U. Z -> ( Z C_ ran F -> Z = ran F ) ) )
120 119 com23 
 |-  ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) -> ( Z C_ ran F -> ( A C_ U. Z -> Z = ran F ) ) )
121 120 imp32 
 |-  ( ( ( F Fn A /\ A. p e. A ( ( F ` p ) i^i A ) = { p } ) /\ ( Z C_ ran F /\ A C_ U. Z ) ) -> Z = ran F )