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