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

Metamath Proof Explorer

Theorem dff4

Description: Alternate definition of a mapping. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion dff4 ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )

Proof

Step Hyp Ref Expression
1 dff3 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) )
2 df-br ⊢ ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
3 ssel ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
4 opelxp2 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → 𝑦 ∈ 𝐵 )
5 3 4 syl6 ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑦 ∈ 𝐵 ) )
6 2 5 biimtrid ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑥 𝐹 𝑦 → 𝑦 ∈ 𝐵 ) )
7 6 pm4.71rd ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑥 𝐹 𝑦 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
8 7 eubidv ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) ) )
9 df-reu ⊢ ( ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑥 𝐹 𝑦 ) )
10 8 9 bitr4di ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )
11 10 ralbidv ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )
12 11 pm5.32i ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )
13 1 12 bitri ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 𝐹 𝑦 ) )