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	bitrid	⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
30	29	bian1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
32	4	fveq1i	⊢ ( 𝐹 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
33	2	fvmpt2f	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
34	32 33	eqtrid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
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	bitrid	⊢ ( 𝜑 → ( Fun ^◡ 𝐹 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )

Metamath Proof Explorer

Theorem funcnvmpt

Proof