This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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