Theorem f1opr 7076

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

Assertion

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

Distinct variable groups:   𝐴,𝑟,𝑠,𝑡,𝑢   𝐵,𝑟,𝑠,𝑡,𝑢   𝐹,𝑟,𝑠,𝑡,𝑢

Allowed substitution hints:   𝐶(𝑢,𝑡,𝑠,𝑟)

Proof of Theorem f1opr

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dff13 6885	. 2 ⊢ (𝐹:(𝐴 × 𝐵)–1-1→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑣 ∈ (𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤)))
2		fveq2 6545	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑟, 𝑠⟩ → (𝐹‘𝑣) = (𝐹‘⟨𝑟, 𝑠⟩))
3		df-ov 7026	. . . . . . . . 9 ⊢ (𝑟𝐹𝑠) = (𝐹‘⟨𝑟, 𝑠⟩)
4	2, 3	syl6eqr 2851	. . . . . . . 8 ⊢ (𝑣 = ⟨𝑟, 𝑠⟩ → (𝐹‘𝑣) = (𝑟𝐹𝑠))
5	4	eqeq1d 2799	. . . . . . 7 ⊢ (𝑣 = ⟨𝑟, 𝑠⟩ → ((𝐹‘𝑣) = (𝐹‘𝑤) ↔ (𝑟𝐹𝑠) = (𝐹‘𝑤)))
6		eqeq1 2801	. . . . . . 7 ⊢ (𝑣 = ⟨𝑟, 𝑠⟩ → (𝑣 = 𝑤 ↔ ⟨𝑟, 𝑠⟩ = 𝑤))
7	5, 6	imbi12d 346	. . . . . 6 ⊢ (𝑣 = ⟨𝑟, 𝑠⟩ → (((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤) ↔ ((𝑟𝐹𝑠) = (𝐹‘𝑤) → ⟨𝑟, 𝑠⟩ = 𝑤)))
8	7	ralbidv 3166	. . . . 5 ⊢ (𝑣 = ⟨𝑟, 𝑠⟩ → (∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤) ↔ ∀𝑤 ∈ (𝐴 × 𝐵)((𝑟𝐹𝑠) = (𝐹‘𝑤) → ⟨𝑟, 𝑠⟩ = 𝑤)))
9	8	ralxp 5605	. . . 4 ⊢ (∀𝑣 ∈ (𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤) ↔ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑤 ∈ (𝐴 × 𝐵)((𝑟𝐹𝑠) = (𝐹‘𝑤) → ⟨𝑟, 𝑠⟩ = 𝑤))
10		fveq2 6545	. . . . . . . . 9 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (𝐹‘𝑤) = (𝐹‘⟨𝑡, 𝑢⟩))
11		df-ov 7026	. . . . . . . . 9 ⊢ (𝑡𝐹𝑢) = (𝐹‘⟨𝑡, 𝑢⟩)
12	10, 11	syl6eqr 2851	. . . . . . . 8 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (𝐹‘𝑤) = (𝑡𝐹𝑢))
13	12	eqeq2d 2807	. . . . . . 7 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑟𝐹𝑠) = (𝐹‘𝑤) ↔ (𝑟𝐹𝑠) = (𝑡𝐹𝑢)))
14		eqeq2 2808	. . . . . . . 8 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (⟨𝑟, 𝑠⟩ = 𝑤 ↔ ⟨𝑟, 𝑠⟩ = ⟨𝑡, 𝑢⟩))
15		vex 3443	. . . . . . . . 9 ⊢ 𝑟 ∈ V
16		vex 3443	. . . . . . . . 9 ⊢ 𝑠 ∈ V
17	15, 16	opth 5267	. . . . . . . 8 ⊢ (⟨𝑟, 𝑠⟩ = ⟨𝑡, 𝑢⟩ ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
18	14, 17	syl6bb 288	. . . . . . 7 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (⟨𝑟, 𝑠⟩ = 𝑤 ↔ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
19	13, 18	imbi12d 346	. . . . . 6 ⊢ (𝑤 = ⟨𝑡, 𝑢⟩ → (((𝑟𝐹𝑠) = (𝐹‘𝑤) → ⟨𝑟, 𝑠⟩ = 𝑤) ↔ ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))))
20	19	ralxp 5605	. . . . 5 ⊢ (∀𝑤 ∈ (𝐴 × 𝐵)((𝑟𝐹𝑠) = (𝐹‘𝑤) → ⟨𝑟, 𝑠⟩ = 𝑤) ↔ ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
21	20	2ralbii 3135	. . . 4 ⊢ (∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑤 ∈ (𝐴 × 𝐵)((𝑟𝐹𝑠) = (𝐹‘𝑤) → ⟨𝑟, 𝑠⟩ = 𝑤) ↔ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
22	9, 21	bitri 276	. . 3 ⊢ (∀𝑣 ∈ (𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤) ↔ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
23	22	anbi2i 622	. 2 ⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑣 ∈ (𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤)) ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))))
24	1, 23	bitri 276	1 ⊢ (𝐹:(𝐴 × 𝐵)–1-1→𝐶 ↔ (𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ ∀𝑟 ∈ 𝐴 ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ∀𝑢 ∈ 𝐵 ((𝑟𝐹𝑠) = (𝑡𝐹𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1525  ∀wral 3107  ⟨cop 4484   × cxp 5448  ⟶wf 6228  –1-1→wf1 6229  ‘cfv 6232  (class class class)co 7023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fv 6240  df-ov 7026

This theorem is referenced by:  fedgmul  30627