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 𝐹 ↔ ∀ 𝑖𝐴𝑗𝐴 ( 𝑖 = 𝑗 𝑖 / 𝑥 𝐵 𝑗 / 𝑥 𝐵 ) ) )