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