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 ⊢ Ⅎ _ x A
funcnvmpt.2 ⊢ Ⅎ _ x F
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 ∈ A x = z ∨ B ≠ C

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