Metamath Proof Explorer

Theorem f1opr

Description: Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010)

Ref Expression
Assertion f1opr ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1→ 𝐶 ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑟 ∈ 𝐴 ∀ 𝑠 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ∀ 𝑢 ∈ 𝐵 ( ( 𝑟 𝐹 𝑠 ) = ( 𝑡 𝐹 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) ) )

Proof

Step Hyp Ref Expression
1 dff13 ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1→ 𝐶 ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) )
2 fveq2 ⊢ ( 𝑣 = ⟨ 𝑟 , 𝑠 ⟩ → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ ⟨ 𝑟 , 𝑠 ⟩ ) )
3 df-ov ⊢ ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ ⟨ 𝑟 , 𝑠 ⟩ )
4 2 3 eqtr4di ⊢ ( 𝑣 = ⟨ 𝑟 , 𝑠 ⟩ → ( 𝐹 ‘ 𝑣 ) = ( 𝑟 𝐹 𝑠 ) )
5 4 eqeq1d ⊢ ( 𝑣 = ⟨ 𝑟 , 𝑠 ⟩ → ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ 𝑤 ) ) )
6 eqeq1 ⊢ ( 𝑣 = ⟨ 𝑟 , 𝑠 ⟩ → ( 𝑣 = 𝑤 ↔ ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ) )
7 5 6 imbi12d ⊢ ( 𝑣 = ⟨ 𝑟 , 𝑠 ⟩ → ( ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ↔ ( ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ 𝑤 ) → ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ) ) )
8 7 ralbidv ⊢ ( 𝑣 = ⟨ 𝑟 , 𝑠 ⟩ → ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ↔ ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ 𝑤 ) → ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ) ) )
9 8 ralxp ⊢ ( ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ↔ ∀ 𝑟 ∈ 𝐴 ∀ 𝑠 ∈ 𝐵 ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ 𝑤 ) → ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ) )
10 fveq2 ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ⟨ 𝑡 , 𝑢 ⟩ ) )
11 df-ov ⊢ ( 𝑡 𝐹 𝑢 ) = ( 𝐹 ‘ ⟨ 𝑡 , 𝑢 ⟩ )
12 10 11 eqtr4di ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( 𝐹 ‘ 𝑤 ) = ( 𝑡 𝐹 𝑢 ) )
13 12 eqeq2d ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝑟 𝐹 𝑠 ) = ( 𝑡 𝐹 𝑢 ) ) )
14 eqeq2 ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ↔ ⟨ 𝑟 , 𝑠 ⟩ = ⟨ 𝑡 , 𝑢 ⟩ ) )
15 vex ⊢ 𝑟 ∈ V
16 vex ⊢ 𝑠 ∈ V
17 15 16 opth ⊢ ( ⟨ 𝑟 , 𝑠 ⟩ = ⟨ 𝑡 , 𝑢 ⟩ ↔ ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) )
18 14 17 bitrdi ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ↔ ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) )
19 13 18 imbi12d ⊢ ( 𝑤 = ⟨ 𝑡 , 𝑢 ⟩ → ( ( ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ 𝑤 ) → ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ) ↔ ( ( 𝑟 𝐹 𝑠 ) = ( 𝑡 𝐹 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) ) )
20 19 ralxp ⊢ ( ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ 𝑤 ) → ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ) ↔ ∀ 𝑡 ∈ 𝐴 ∀ 𝑢 ∈ 𝐵 ( ( 𝑟 𝐹 𝑠 ) = ( 𝑡 𝐹 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) )
21 20 2ralbii ⊢ ( ∀ 𝑟 ∈ 𝐴 ∀ 𝑠 ∈ 𝐵 ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝑟 𝐹 𝑠 ) = ( 𝐹 ‘ 𝑤 ) → ⟨ 𝑟 , 𝑠 ⟩ = 𝑤 ) ↔ ∀ 𝑟 ∈ 𝐴 ∀ 𝑠 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ∀ 𝑢 ∈ 𝐵 ( ( 𝑟 𝐹 𝑠 ) = ( 𝑡 𝐹 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) )
22 9 21 bitri ⊢ ( ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ↔ ∀ 𝑟 ∈ 𝐴 ∀ 𝑠 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ∀ 𝑢 ∈ 𝐵 ( ( 𝑟 𝐹 𝑠 ) = ( 𝑡 𝐹 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) )
23 22 anbi2i ⊢ ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑤 ∈ ( 𝐴 × 𝐵 ) ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑟 ∈ 𝐴 ∀ 𝑠 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ∀ 𝑢 ∈ 𝐵 ( ( 𝑟 𝐹 𝑠 ) = ( 𝑡 𝐹 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) ) )
24 1 23 bitri ⊢ ( 𝐹 : ( 𝐴 × 𝐵 ) –1-1→ 𝐶 ↔ ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐶 ∧ ∀ 𝑟 ∈ 𝐴 ∀ 𝑠 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ∀ 𝑢 ∈ 𝐵 ( ( 𝑟 𝐹 𝑠 ) = ( 𝑡 𝐹 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) ) )