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

Metamath Proof Explorer

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 eqabf ⊢ ( 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 = 𝐵 ) ) )
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 𝐴 )