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

Proof

Step	Hyp	Ref	Expression
1		funcnv5mpt.0	⊢ Ⅎ 𝑥 𝜑
2		funcnv5mpt.1	⊢ Ⅎ 𝑥 𝐴
3		funcnv5mpt.2	⊢ Ⅎ 𝑥 𝐹
4		funcnv5mpt.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5		funcnv5mpt.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
6		funcnv5mpt.5	⊢ ( 𝑥 = 𝑧 → 𝐵 = 𝐶 )
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 ^◡ 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶 ) ) )

Metamath Proof Explorer

Theorem funcnv5mpt

Proof