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

Metamath Proof Explorer

Theorem f1ofveu

Description: There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006)

Ref Expression
Assertion f1ofveu ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B → ∃! x ∈ A F ⁡ x = C

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A
2 f1of ⊢ F -1 : B ⟶ 1-1 onto A → F -1 : B ⟶ A
3 1 2 syl ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ A
4 feu ⊢ F -1 : B ⟶ A ∧ C ∈ B → ∃! x ∈ A C x ∈ F -1
5 3 4 sylan ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B → ∃! x ∈ A C x ∈ F -1
6 f1ocnvfvb ⊢ F : A ⟶ 1-1 onto B ∧ x ∈ A ∧ C ∈ B → F ⁡ x = C ↔ F -1 ⁡ C = x
7 6 3com23 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B ∧ x ∈ A → F ⁡ x = C ↔ F -1 ⁡ C = x
8 dff1o4 ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ F -1 Fn B
9 8 simprbi ⊢ F : A ⟶ 1-1 onto B → F -1 Fn B
10 fnopfvb ⊢ F -1 Fn B ∧ C ∈ B → F -1 ⁡ C = x ↔ C x ∈ F -1
11 10 3adant3 ⊢ F -1 Fn B ∧ C ∈ B ∧ x ∈ A → F -1 ⁡ C = x ↔ C x ∈ F -1
12 9 11 syl3an1 ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B ∧ x ∈ A → F -1 ⁡ C = x ↔ C x ∈ F -1
13 7 12 bitrd ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B ∧ x ∈ A → F ⁡ x = C ↔ C x ∈ F -1
14 13 3expa ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B ∧ x ∈ A → F ⁡ x = C ↔ C x ∈ F -1
15 14 reubidva ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B → ∃! x ∈ A F ⁡ x = C ↔ ∃! x ∈ A C x ∈ F -1
16 5 15 mpbird ⊢ F : A ⟶ 1-1 onto B ∧ C ∈ B → ∃! x ∈ A F ⁡ x = C