Metamath Proof Explorer

Theorem funcnv5mpt

Description: Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-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
funcnv5mpt.1 ⊢x=z→B=C
Assertion funcnv5mpt ⊢φ→Fun⁡F-1↔∀x∈A∀z∈Ax=z∨B≠C

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 funcnv5mpt.1 ⊢x=z→B=C
7 1 2 3 4 5 funcnvmpt ⊢φ→Fun⁡F-1↔∀y∃*x∈Ay=B
8 nne ⊢¬B≠C↔B=C
9 eqvincg ⊢B∈V→B=C↔∃yy=B∧y=C
10 5 9 syl ⊢φ∧x∈A→B=C↔∃yy=B∧y=C
11 8 10 bitrid ⊢φ∧x∈A→¬B≠C↔∃yy=B∧y=C
12 11 imbi1d ⊢φ∧x∈A→¬B≠C→x=z↔∃yy=B∧y=C→x=z
13 orcom ⊢x=z∨B≠C↔B≠C∨x=z
14 df-or ⊢B≠C∨x=z↔¬B≠C→x=z
15 13 14 bitri ⊢x=z∨B≠C↔¬B≠C→x=z
16 19.23v ⊢∀yy=B∧y=C→x=z↔∃yy=B∧y=C→x=z
17 12 15 16 3bitr4g ⊢φ∧x∈A→x=z∨B≠C↔∀yy=B∧y=C→x=z
18 17 ralbidv ⊢φ∧x∈A→∀z∈Ax=z∨B≠C↔∀z∈A∀yy=B∧y=C→x=z
19 ralcom4 ⊢∀z∈A∀yy=B∧y=C→x=z↔∀y∀z∈Ay=B∧y=C→x=z
20 18 19 bitrdi ⊢φ∧x∈A→∀z∈Ax=z∨B≠C↔∀y∀z∈Ay=B∧y=C→x=z
21 1 20 ralbida ⊢φ→∀x∈A∀z∈Ax=z∨B≠C↔∀x∈A∀y∀z∈Ay=B∧y=C→x=z
22 nfcv ⊢Ⅎ_zA
23 nfv ⊢Ⅎxy=C
24 6 eqeq2d ⊢x=z→y=B↔y=C
25 2 22 23 24 rmo4f ⊢∃*x∈Ay=B↔∀x∈A∀z∈Ay=B∧y=C→x=z
26 25 albii ⊢∀y∃*x∈Ay=B↔∀y∀x∈A∀z∈Ay=B∧y=C→x=z
27 ralcom4 ⊢∀x∈A∀y∀z∈Ay=B∧y=C→x=z↔∀y∀x∈A∀z∈Ay=B∧y=C→x=z
28 26 27 bitr4i ⊢∀y∃*x∈Ay=B↔∀x∈A∀y∀z∈Ay=B∧y=C→x=z
29 21 28 bitr4di ⊢φ→∀x∈A∀z∈Ax=z∨B≠C↔∀y∃*x∈Ay=B
30 7 29 bitr4d ⊢φ→Fun⁡F-1↔∀x∈A∀z∈Ax=z∨B≠C