Metamath Proof Explorer


Theorem funcnvmpt

Description: Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017)

Ref Expression
Hypotheses funcnvmpt.0 x φ
funcnvmpt.1 _ x A
funcnvmpt.2 _ x F
funcnvmpt.3 F = x A B
funcnvmpt.4 φ x A B V
Assertion funcnvmpt φ Fun F -1 y * x A y = B

Proof

Step Hyp Ref Expression
1 funcnvmpt.0 x φ
2 funcnvmpt.1 _ x A
3 funcnvmpt.2 _ x F
4 funcnvmpt.3 F = x A B
5 funcnvmpt.4 φ x A B V
6 relcnv Rel F -1
7 nfcv _ y F -1
8 3 nfcnv _ x F -1
9 7 8 dffun6f Fun F -1 Rel F -1 y * x y F -1 x
10 6 9 mpbiran Fun F -1 y * x y F -1 x
11 vex y V
12 vex x V
13 11 12 brcnv y F -1 x x F y
14 13 mobii * x y F -1 x * x x F y
15 14 albii y * x y F -1 x y * x x F y
16 10 15 bitri Fun F -1 y * x x F y
17 4 funmpt2 Fun F
18 funbrfv2b Fun F x F y x dom F F x = y
19 17 18 ax-mp x F y x dom F F x = y
20 4 dmmpt dom F = x A | B V
21 5 elexd φ x A B V
22 21 ex φ x A B V
23 1 22 ralrimi φ x A B V
24 2 rabid2f A = x A | B V x A B V
25 23 24 sylibr φ A = x A | B V
26 20 25 eqtr4id φ dom F = A
27 26 eleq2d φ x dom F x A
28 27 anbi1d φ x dom F F x = y x A F x = y
29 19 28 syl5bb φ x F y x A F x = y
30 29 bian1d φ x A x F y x A F x = y
31 simpr φ x A x A
32 4 fveq1i F x = x A B x
33 2 fvmpt2f x A B V x A B x = B
34 32 33 syl5eq x A B V F x = B
35 31 5 34 syl2anc φ x A F x = B
36 35 eqeq2d φ x A y = F x y = B
37 eqcom F x = y y = F x
38 27 biimpar φ x A x dom F
39 funbrfvb Fun F x dom F F x = y x F y
40 17 38 39 sylancr φ x A F x = y x F y
41 37 40 bitr3id φ x A y = F x x F y
42 36 41 bitr3d φ x A y = B x F y
43 42 pm5.32da φ x A y = B x A x F y
44 30 43 29 3bitr4rd φ x F y x A y = B
45 1 44 mobid φ * x x F y * x x A y = B
46 df-rmo * x A y = B * x x A y = B
47 45 46 bitr4di φ * x x F y * x A y = B
48 47 albidv φ y * x x F y y * x A y = B
49 16 48 syl5bb φ Fun F -1 y * x A y = B