Theorem funcnv4mpt

Description: Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017)

	Ref	Expression
Hypotheses	funcnvmpt.0	⊢ Ⅎ 𝑥 𝜑
	funcnvmpt.1	⊢ Ⅎ 𝑥 𝐴
	funcnvmpt.2	⊢ Ⅎ 𝑥 𝐹
	funcnvmpt.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	funcnvmpt.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion	funcnv4mpt	⊢ ( 𝜑 → ( Fun ◡ 𝐹 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funcnvmpt.0	⊢ Ⅎ 𝑥 𝜑
2		funcnvmpt.1	⊢ Ⅎ 𝑥 𝐴
3		funcnvmpt.2	⊢ Ⅎ 𝑥 𝐹
4		funcnvmpt.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5		funcnvmpt.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
6		nfv	⊢ Ⅎ 𝑖 𝜑
7		nfcv	⊢ Ⅎ 𝑖 𝐴
8		nfcv	⊢ Ⅎ 𝑖 𝐹
9		nfcv	⊢ Ⅎ 𝑖 𝐵
10		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ 𝐵
11		csbeq1a	⊢ ( 𝑥 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
12	2 7 9 10 11	cbvmptf	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
13	4 12	eqtri	⊢ 𝐹 = ( 𝑖 ∈ 𝐴 ↦ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
14	5	sbimi	⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑖 / 𝑥 ] 𝐵 ∈ 𝑉 )
15		nfcv	⊢ Ⅎ 𝑥 𝑖
16	15 2	nfel	⊢ Ⅎ 𝑥 𝑖 ∈ 𝐴
17	1 16	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑖 ∈ 𝐴 )
18		eleq1w	⊢ ( 𝑥 = 𝑖 → ( 𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 ) )
19	18	anbi2d	⊢ ( 𝑥 = 𝑖 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ) )
20	17 19	sbiev	⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) )
21		nfcv	⊢ Ⅎ 𝑥 𝑉
22	10 21	nfel	⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∈ 𝑉
23	11	eleq1d	⊢ ( 𝑥 = 𝑖 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) )
24	22 23	sbiev	⊢ ( [ 𝑖 / 𝑥 ] 𝐵 ∈ 𝑉 ↔ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
25	14 20 24	3imtr3i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
26		csbeq1	⊢ ( 𝑖 = 𝑗 → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 = ⦋ 𝑗 / 𝑥 ⦌ 𝐵 )
27	6 7 8 13 25 26	funcnv5mpt	⊢ ( 𝜑 → ( Fun ◡ 𝐹 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ) )