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

Metamath Proof Explorer

Theorem foov

Description: An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006)

Ref Expression
Assertion foov ( 𝐹 : ( 𝐴 × 𝐵 ) –onto→ 𝐶 ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑧 ∈ 𝐶 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 dffo3 ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –onto→ 𝐶 ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ ( 𝐴 × 𝐵 ) 𝑧 = ( 𝐹 ‘ 𝑤 ) ) )
2 fveq2 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
3 df-ov ⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4 2 3 eqtr4di ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ 𝑤 ) = ( 𝑥 𝐹 𝑦 ) )
5 4 eqeq2d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )
6 5 rexxp ⊢ ( ∃ 𝑤 ∈ ( 𝐴 × 𝐵 ) 𝑧 = ( 𝐹 ‘ 𝑤 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) )
7 6 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ ( 𝐴 × 𝐵 ) 𝑧 = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑧 ∈ 𝐶 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) )
8 7 anbi2i ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ ( 𝐴 × 𝐵 ) 𝑧 = ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑧 ∈ 𝐶 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )
9 1 8 bitri ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –onto→ 𝐶 ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑧 ∈ 𝐶 ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = ( 𝑥 𝐹 𝑦 ) ) )