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

Metamath Proof Explorer

Theorem fnopabg

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 30-Jan-2004) (Proof shortened by Mario Carneiro, 4-Dec-2016)

Ref Expression
Hypothesis fnopabg.1 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
Assertion fnopabg ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ↔ 𝐹 Fn 𝐴 )

Proof

Step Hyp Ref Expression
1 fnopabg.1 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2 moanimv ⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 ) )
3 2 albii ⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 ) )
4 funopab ⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
5 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝜑 ) )
6 3 4 5 3bitr4ri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝜑 ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
7 dmopab3 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 )
8 6 7 anbi12i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ) ↔ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 ) )
9 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃* 𝑦 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝜑 ) )
10 df-fn ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } Fn 𝐴 ↔ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∧ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = 𝐴 ) )
11 8 9 10 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃* 𝑦 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } Fn 𝐴 )
12 df-eu ⊢ ( ∃! 𝑦 𝜑 ↔ ( ∃ 𝑦 𝜑 ∧ ∃* 𝑦 𝜑 ) )
13 12 biancomi ⊢ ( ∃! 𝑦 𝜑 ↔ ( ∃* 𝑦 𝜑 ∧ ∃ 𝑦 𝜑 ) )
14 13 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ( ∃* 𝑦 𝜑 ∧ ∃ 𝑦 𝜑 ) )
15 1 fneq1i ⊢ ( 𝐹 Fn 𝐴 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } Fn 𝐴 )
16 11 14 15 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝜑 ↔ 𝐹 Fn 𝐴 )