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 ⊢Ⅎ_xA
funcnvmpt.2 ⊢Ⅎ_xF
funcnvmpt.3 ⊢F=x∈A⟼B
funcnvmpt.4 ⊢φ∧x∈A→B∈V
Assertion funcnv4mpt ⊢φ→Fun⁡F-1↔∀i∈A∀j∈Ai=j∨⦋i/x⦌B≠⦋j/x⦌B

Proof

Step Hyp Ref Expression
1 funcnvmpt.0 ⊢Ⅎxφ
2 funcnvmpt.1 ⊢Ⅎ_xA
3 funcnvmpt.2 ⊢Ⅎ_xF
4 funcnvmpt.3 ⊢F=x∈A⟼B
5 funcnvmpt.4 ⊢φ∧x∈A→B∈V
6 nfv ⊢Ⅎiφ
7 nfcv ⊢Ⅎ_iA
8 nfcv ⊢Ⅎ_iF
9 nfcv ⊢Ⅎ_iB
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 ⊢ixφ∧x∈A→ixB∈V
15 nfcv ⊢Ⅎ_xi
16 15 2 nfel ⊢Ⅎxi∈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 ⊢ixφ∧x∈A↔φ∧i∈A
21 nfcv ⊢Ⅎ_xV
22 10 21 nfel ⊢Ⅎx⦋i/x⦌B∈V
23 11 eleq1d ⊢x=i→B∈V↔⦋i/x⦌B∈V
24 22 23 sbiev ⊢ixB∈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∈Ai=j∨⦋i/x⦌B≠⦋j/x⦌B