Metamath Proof Explorer

Theorem fodmrnu

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

Ref Expression
Assertion fodmrnu ⊢ F : A ⟶ onto B ∧ F : C ⟶ onto D → A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 fofn ⊢ F : A ⟶ onto B → F Fn A
2 fofn ⊢ F : C ⟶ onto D → F Fn C
3 fndmu ⊢ F Fn A ∧ F Fn C → A = C
4 1 2 3 syl2an ⊢ F : A ⟶ onto B ∧ F : C ⟶ onto D → A = C
5 forn ⊢ F : A ⟶ onto B → ran ⁡ F = B
6 forn ⊢ F : C ⟶ onto D → ran ⁡ F = D
7 5 6 sylan9req ⊢ F : A ⟶ onto B ∧ F : C ⟶ onto D → B = D
8 4 7 jca ⊢ F : A ⟶ onto B ∧ F : C ⟶ onto D → A = C ∧ B = D