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 𝑥 𝜑
funcnvmpt.1 𝑥 𝐴
funcnvmpt.2 𝑥 𝐹
funcnvmpt.3 𝐹 = ( 𝑥𝐴𝐵 )
funcnvmpt.4 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
Assertion funcnvmpt ( 𝜑 → ( Fun 𝐹 ↔ ∀ 𝑦 ∃* 𝑥𝐴 𝑦 = 𝐵 ) )

Proof

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