This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ◡ 𝐹 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ) )