Theorem fodmrnu 6832

Description: An onto function has unique domain and range. (Contributed by NM, 5-Nov-2006.)

Assertion

Ref	Expression
fodmrnu	⊢ ((𝐹:𝐴⟶onto𝐵 ∧ 𝐹:𝐶⟶onto𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))

Proof of Theorem fodmrnu

Step	Hyp	Ref	Expression
1		fofn 6826	. . 3 ⊢ (𝐹:𝐴⟶onto𝐵 → 𝐹 Fn 𝐴)
2		fofn 6826	. . 3 ⊢ (𝐹:𝐶⟶onto𝐷 → 𝐹 Fn 𝐶)
3		fndmu 6674	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐶) → 𝐴 = 𝐶)
4	1, 2, 3	syl2an 608	. 2 ⊢ ((𝐹:𝐴⟶onto𝐵 ∧ 𝐹:𝐶⟶onto𝐷) → 𝐴 = 𝐶)
5		forn 6827	. . 3 ⊢ (𝐹:𝐴⟶onto𝐵 → ran 𝐹 = 𝐵)
6		forn 6827	. . 3 ⊢ (𝐹:𝐶⟶onto𝐷 → ran 𝐹 = 𝐷)
7	5, 6	sylan9req 2819	. 2 ⊢ ((𝐹:𝐴⟶onto𝐵 ∧ 𝐹:𝐶⟶onto𝐷) → 𝐵 = 𝐷)
8	4, 7	jca 521	1 ⊢ ((𝐹:𝐴⟶onto𝐵 ∧ 𝐹:𝐶⟶onto𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ran crn 5657   Fn wfn 6559  ⟶ontowfo 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-fn 6567  df-f 6568  df-fo 6570

This theorem is used by: (None)