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 x φ
funcnvmpt.1 _ x A
funcnvmpt.2 _ x F
funcnvmpt.3 F = x A B
funcnvmpt.4 φ x A B V
Assertion funcnv4mpt φ Fun F -1 i A j A i = j i / x B j / x B

Proof

Step Hyp Ref Expression
1 funcnvmpt.0 x φ
2 funcnvmpt.1 _ x A
3 funcnvmpt.2 _ x F
4 funcnvmpt.3 F = x A B
5 funcnvmpt.4 φ x A B V
6 nfv i φ
7 nfcv _ i A
8 nfcv _ i F
9 nfcv _ i B
10 nfcsb1v _ x i / x B
11 csbeq1a x = i B = i / x B
12 2 7 9 10 11 cbvmptf x A B = i A i / x B
13 4 12 eqtri F = i A i / x B
14 5 sbimi i x φ x A i x B V
15 nfcv _ x i
16 15 2 nfel x i A
17 1 16 nfan x φ i A
18 eleq1w x = i x A i A
19 18 anbi2d x = i φ x A φ i A
20 17 19 sbiev i x φ x A φ i A
21 nfcv _ x V
22 10 21 nfel x i / x B V
23 11 eleq1d x = i B V i / x B V
24 22 23 sbiev i x B V i / x B V
25 14 20 24 3imtr3i φ i A i / x B V
26 csbeq1 i = j i / x B = j / x B
27 6 7 8 13 25 26 funcnv5mpt φ Fun F -1 i A j A i = j i / x B j / x B