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

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 ⊢ Ⅎ 𝑥 𝜑
funcnvmpt.1 ⊢ Ⅎ 𝑥 𝐴
funcnvmpt.2 ⊢ Ⅎ 𝑥 𝐹
funcnvmpt.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
funcnvmpt.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
funcnv5mpt.1 ⊢ ( 𝑥 = 𝑧 → 𝐵 = 𝐶 )
Assertion funcnv5mpt ( 𝜑 → ( Fun ◡ 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 funcnvmpt.0 ⊢ Ⅎ 𝑥 𝜑
2 funcnvmpt.1 ⊢ Ⅎ 𝑥 𝐴
3 funcnvmpt.2 ⊢ Ⅎ 𝑥 𝐹
4 funcnvmpt.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5 funcnvmpt.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
6 funcnv5mpt.1 ⊢ ( 𝑥 = 𝑧 → 𝐵 = 𝐶 )
7 1 2 3 4 5 funcnvmpt ⊢ ( 𝜑 → ( Fun ◡ 𝐹 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
8 nne ⊢ ( ¬ 𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶 )
9 eqvincg ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 = 𝐶 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) ) )
10 5 9 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 = 𝐶 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) ) )
11 8 10 bitrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝐵 ≠ 𝐶 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) ) )
12 11 imbi1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ¬ 𝐵 ≠ 𝐶 → 𝑥 = 𝑧 ) ↔ ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) ) )
13 orcom ⊢ ( ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ↔ ( 𝐵 ≠ 𝐶 ∨ 𝑥 = 𝑧 ) )
14 df-or ⊢ ( ( 𝐵 ≠ 𝐶 ∨ 𝑥 = 𝑧 ) ↔ ( ¬ 𝐵 ≠ 𝐶 → 𝑥 = 𝑧 ) )
15 13 14 bitri ⊢ ( ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ↔ ( ¬ 𝐵 ≠ 𝐶 → 𝑥 = 𝑧 ) )
16 19.23v ⊢ ( ∀ 𝑦 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) ↔ ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) )
17 12 15 16 3bitr4g ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ↔ ∀ 𝑦 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) ) )
18 17 ralbidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) ) )
19 ralcom4 ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) )
20 18 19 bitrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ↔ ∀ 𝑦 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) ) )
21 1 20 ralbida ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) ) )
22 nfcv ⊢ Ⅎ 𝑧 𝐴
23 nfv ⊢ Ⅎ 𝑥 𝑦 = 𝐶
24 6 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑦 = 𝐶 ) )
25 2 22 23 24 rmo4f ⊢ ( ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) )
26 25 albii ⊢ ( ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) )
27 ralcom4 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) )
28 26 27 bitr4i ⊢ ( ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∀ 𝑧 ∈ 𝐴 ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐶 ) → 𝑥 = 𝑧 ) )
29 21 28 bitr4di ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
30 7 29 bitr4d ⊢ ( 𝜑 → ( Fun ◡ 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ) )