Metamath Proof Explorer

Theorem fvineqsneu

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

Ref Expression
Assertion fvineqsneu ⊢FFnA∧∀p∈AF⁡p∩A=p→∀q∈A∃!x∈ran⁡Fq∈x

Proof

Step Hyp Ref Expression
1 fnfvelrn ⊢FFnA∧o∈A→F⁡o∈ran⁡F
2 1 ex ⊢FFnA→o∈A→F⁡o∈ran⁡F
3 2 adantr ⊢FFnA∧∀p∈AF⁡p∩A=p→o∈A→F⁡o∈ran⁡F
4 fnrnfv ⊢FFnA→ran⁡F=y|∃p∈Ay=F⁡p
5 4 eqabrd ⊢FFnA→y∈ran⁡F↔∃p∈Ay=F⁡p
6 5 adantr ⊢FFnA∧∀p∈AF⁡p∩A=p→y∈ran⁡F↔∃p∈Ay=F⁡p
7 nfv ⊢ℲpFFnA
8 nfra1 ⊢Ⅎp∀p∈AF⁡p∩A=p
9 7 8 nfan ⊢ℲpFFnA∧∀p∈AF⁡p∩A=p
10 nfv ⊢Ⅎp∀o∈Ao∈y↔y=F⁡o
11 eleq2 ⊢y=F⁡p→o∈y↔o∈F⁡p
12 elin ⊢o∈F⁡p∩A↔o∈F⁡p∧o∈A
13 12 rbaib ⊢o∈A→o∈F⁡p∩A↔o∈F⁡p
14 13 ad2antll ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A→o∈F⁡p∩A↔o∈F⁡p
15 rsp ⊢∀p∈AF⁡p∩A=p→p∈A→F⁡p∩A=p
16 eleq2 ⊢F⁡p∩A=p→o∈F⁡p∩A↔o∈p
17 velsn ⊢o∈p↔o=p
18 equcom ⊢o=p↔p=o
19 17 18 bitri ⊢o∈p↔p=o
20 16 19 bitrdi ⊢F⁡p∩A=p→o∈F⁡p∩A↔p=o
21 15 20 syl6 ⊢∀p∈AF⁡p∩A=p→p∈A→o∈F⁡p∩A↔p=o
22 21 adantl ⊢FFnA∧∀p∈AF⁡p∩A=p→p∈A→o∈F⁡p∩A↔p=o
23 22 adantrd ⊢FFnA∧∀p∈AF⁡p∩A=p→p∈A∧o∈A→o∈F⁡p∩A↔p=o
24 23 imp ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A→o∈F⁡p∩A↔p=o
25 14 24 bitr3d ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A→o∈F⁡p↔p=o
26 11 25 sylan9bbr ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A∧y=F⁡p→o∈y↔p=o
27 26 ex ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A→y=F⁡p→o∈y↔p=o
28 27 anass1rs ⊢FFnA∧∀p∈AF⁡p∩A=p∧o∈A∧p∈A→y=F⁡p→o∈y↔p=o
29 28 impr ⊢FFnA∧∀p∈AF⁡p∩A=p∧o∈A∧p∈A∧y=F⁡p→o∈y↔p=o
30 29 an32s ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧y=F⁡p∧o∈A→o∈y↔p=o
31 eqeq1 ⊢y=F⁡p→y=F⁡o↔F⁡p=F⁡o
32 dffn3 ⊢FFnA↔F:A⟶ran⁡F
33 fvineqsnf1 ⊢F:A⟶ran⁡F∧∀p∈AF⁡p∩A=p→F:A⟶1-1ran⁡F
34 32 33 sylanb ⊢FFnA∧∀p∈AF⁡p∩A=p→F:A⟶1-1ran⁡F
35 dff13 ⊢F:A⟶1-1ran⁡F↔F:A⟶ran⁡F∧∀p∈A∀o∈AF⁡p=F⁡o→p=o
36 34 35 sylib ⊢FFnA∧∀p∈AF⁡p∩A=p→F:A⟶ran⁡F∧∀p∈A∀o∈AF⁡p=F⁡o→p=o
37 36 simprd ⊢FFnA∧∀p∈AF⁡p∩A=p→∀p∈A∀o∈AF⁡p=F⁡o→p=o
38 rsp ⊢∀p∈A∀o∈AF⁡p=F⁡o→p=o→p∈A→∀o∈AF⁡p=F⁡o→p=o
39 37 38 syl ⊢FFnA∧∀p∈AF⁡p∩A=p→p∈A→∀o∈AF⁡p=F⁡o→p=o
40 rsp ⊢∀o∈AF⁡p=F⁡o→p=o→o∈A→F⁡p=F⁡o→p=o
41 39 40 syl6 ⊢FFnA∧∀p∈AF⁡p∩A=p→p∈A→o∈A→F⁡p=F⁡o→p=o
42 41 imp32 ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A→F⁡p=F⁡o→p=o
43 fveq2 ⊢p=o→F⁡p=F⁡o
44 42 43 impbid1 ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A→F⁡p=F⁡o↔p=o
45 31 44 sylan9bbr ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A∧y=F⁡p→y=F⁡o↔p=o
46 45 ex ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧o∈A→y=F⁡p→y=F⁡o↔p=o
47 46 anass1rs ⊢FFnA∧∀p∈AF⁡p∩A=p∧o∈A∧p∈A→y=F⁡p→y=F⁡o↔p=o
48 47 impr ⊢FFnA∧∀p∈AF⁡p∩A=p∧o∈A∧p∈A∧y=F⁡p→y=F⁡o↔p=o
49 48 an32s ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧y=F⁡p∧o∈A→y=F⁡o↔p=o
50 30 49 bitr4d ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧y=F⁡p∧o∈A→o∈y↔y=F⁡o
51 50 ex ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧y=F⁡p→o∈A→o∈y↔y=F⁡o
52 51 ralrimiv ⊢FFnA∧∀p∈AF⁡p∩A=p∧p∈A∧y=F⁡p→∀o∈Ao∈y↔y=F⁡o
53 52 exp32 ⊢FFnA∧∀p∈AF⁡p∩A=p→p∈A→y=F⁡p→∀o∈Ao∈y↔y=F⁡o
54 9 10 53 rexlimd ⊢FFnA∧∀p∈AF⁡p∩A=p→∃p∈Ay=F⁡p→∀o∈Ao∈y↔y=F⁡o
55 6 54 sylbid ⊢FFnA∧∀p∈AF⁡p∩A=p→y∈ran⁡F→∀o∈Ao∈y↔y=F⁡o
56 rsp ⊢∀o∈Ao∈y↔y=F⁡o→o∈A→o∈y↔y=F⁡o
57 55 56 syl6 ⊢FFnA∧∀p∈AF⁡p∩A=p→y∈ran⁡F→o∈A→o∈y↔y=F⁡o
58 57 com23 ⊢FFnA∧∀p∈AF⁡p∩A=p→o∈A→y∈ran⁡F→o∈y↔y=F⁡o
59 58 ralrimdv ⊢FFnA∧∀p∈AF⁡p∩A=p→o∈A→∀y∈ran⁡Fo∈y↔y=F⁡o
60 reu6i ⊢F⁡o∈ran⁡F∧∀y∈ran⁡Fo∈y↔y=F⁡o→∃!y∈ran⁡Fo∈y
61 60 ex ⊢F⁡o∈ran⁡F→∀y∈ran⁡Fo∈y↔y=F⁡o→∃!y∈ran⁡Fo∈y
62 3 59 61 syl6c ⊢FFnA∧∀p∈AF⁡p∩A=p→o∈A→∃!y∈ran⁡Fo∈y
63 62 ralrimiv ⊢FFnA∧∀p∈AF⁡p∩A=p→∀o∈A∃!y∈ran⁡Fo∈y
64 nfv ⊢Ⅎxq=o
65 nfv ⊢Ⅎyq=o
66 nfvd ⊢q=o→Ⅎyq∈x
67 nfvd ⊢q=o→Ⅎxo∈y
68 eleq12 ⊢q=o∧x=y→q∈x↔o∈y
69 68 ex ⊢q=o→x=y→q∈x↔o∈y
70 64 65 66 67 69 cbvreud ⊢q=o→∃!x∈ran⁡Fq∈x↔∃!y∈ran⁡Fo∈y
71 70 cbvralvw ⊢∀q∈A∃!x∈ran⁡Fq∈x↔∀o∈A∃!y∈ran⁡Fo∈y
72 63 71 sylibr ⊢FFnA∧∀p∈AF⁡p∩A=p→∀q∈A∃!x∈ran⁡Fq∈x