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 ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ∃! 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
2 f1of ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
3 1 2 syl ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
4 feu ⊢ ( ( ◡ 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ∃! 𝑥 ∈ 𝐴 ⟨ 𝐶 , 𝑥 ⟩ ∈ ◡ 𝐹 )
5 3 4 sylan ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ∃! 𝑥 ∈ 𝐴 ⟨ 𝐶 , 𝑥 ⟩ ∈ ◡ 𝐹 )
6 f1ocnvfvb ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 ) )
7 6 3com23 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 ) )
8 dff1o4 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )
9 8 simprbi ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 Fn 𝐵 )
10 fnopfvb ⊢ ( ( ◡ 𝐹 Fn 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ ◡ 𝐹 ) )
11 10 3adant3 ⊢ ( ( ◡ 𝐹 Fn 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ ◡ 𝐹 ) )
12 9 11 syl3an1 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( ◡ 𝐹 ‘ 𝐶 ) = 𝑥 ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ ◡ 𝐹 ) )
13 7 12 bitrd ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ ◡ 𝐹 ) )
14 13 3expa ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ⟨ 𝐶 , 𝑥 ⟩ ∈ ◡ 𝐹 ) )
15 14 reubidva ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( ∃! 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ∃! 𝑥 ∈ 𝐴 ⟨ 𝐶 , 𝑥 ⟩ ∈ ◡ 𝐹 ) )
16 5 15 mpbird ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ∃! 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐶 )