Theorem mptfnf

Description: The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011) (Revised by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypothesis	mptfnf.0	⊢ Ⅎ 𝑥 𝐴
Assertion	mptfnf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mptfnf.0	⊢ Ⅎ 𝑥 𝐴
2		eueq	⊢ ( 𝐵 ∈ V ↔ ∃! 𝑦 𝑦 = 𝐵 )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑦 = 𝐵 )
4		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝑦 = 𝐵 ∧ ∃* 𝑦 𝑦 = 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑦 = 𝐵 ) )
5		df-eu	⊢ ( ∃! 𝑦 𝑦 = 𝐵 ↔ ( ∃ 𝑦 𝑦 = 𝐵 ∧ ∃* 𝑦 𝑦 = 𝐵 ) )
6	5	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑦 = 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝑦 = 𝐵 ∧ ∃* 𝑦 𝑦 = 𝐵 ) )
7		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
8	7	fneq1i	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } Fn 𝐴 )
9		df-fn	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } Fn 𝐴 ↔ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = 𝐴 ) )
10	8 9	bitri	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ↔ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = 𝐴 ) )
11		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑦 = 𝐵 ) )
12	11	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑦 = 𝐵 ) )
13		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) )
14		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑦 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑦 = 𝐵 ) )
15	12 13 14	3bitr4ri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑦 = 𝐵 ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } )
16		eqcom	⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) } = 𝐴 ↔ 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) } )
17		dmopab	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
18		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) )
19	18	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) }
20	17 19	eqtri	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) }
21	20	eqeq1i	⊢ ( dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = 𝐴 ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) } = 𝐴 )
22		pm4.71	⊢ ( ( 𝑥 ∈ 𝐴 → ∃ 𝑦 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) ) )
23	22	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃ 𝑦 𝑦 = 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) ) )
24		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃ 𝑦 𝑦 = 𝐵 ) )
25	1	abeq2f	⊢ ( 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) ) )
26	23 24 25	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ↔ 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) } )
27	16 21 26	3bitr4ri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = 𝐴 )
28	15 27	anbi12i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑦 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ) ↔ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = 𝐴 ) )
29		ancom	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑦 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑦 = 𝐵 ) )
30	10 28 29	3bitr2i	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑦 = 𝐵 ) )
31	4 6 30	3bitr4ri	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑦 = 𝐵 )
32	3 31	bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )