funcnvmpt

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

	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	1 21	ralrimia	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
23	2	rabid2f	⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
24	22 23	sylibr	⊢ ( 𝜑 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } )
25	20 24	eqtr4id	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
26	25	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) )
27	26	anbi1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
28	19 27	bitrid	⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
29	28	bian1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
31	4	fveq1i	⊢ ( 𝐹 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
32	2	fvmpt2f	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
33	31 32	eqtrid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
34	30 5 33	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
35	34	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 = 𝐵 ) )
36		eqcom	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) )
37	26	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐹 )
38		funbrfvb	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
39	17 37 38	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
40	36 39	bitr3id	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
41	35 40	bitr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = 𝐵 ↔ 𝑥 𝐹 𝑦 ) )
42	41	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) )
43	29 42 28	3bitr4rd	⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) )
44	1 43	mobid	⊢ ( 𝜑 → ( ∃* 𝑥 𝑥 𝐹 𝑦 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) )
45		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) )
46	44 45	bitr4di	⊢ ( 𝜑 → ( ∃* 𝑥 𝑥 𝐹 𝑦 ↔ ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
47	46	albidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
48	16 47	bitrid	⊢ ( 𝜑 → ( Fun ^◡ 𝐹 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )

Metamath Proof Explorer

Theorem funcnvmpt

Proof