Metamath Proof Explorer


Theorem f1od

Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014)

Ref Expression
Hypotheses f1od.1 𝐹 = ( 𝑥𝐴𝐶 )
f1od.2 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑊 )
f1od.3 ( ( 𝜑𝑦𝐵 ) → 𝐷𝑋 )
f1od.4 ( 𝜑 → ( ( 𝑥𝐴𝑦 = 𝐶 ) ↔ ( 𝑦𝐵𝑥 = 𝐷 ) ) )
Assertion f1od ( 𝜑𝐹 : 𝐴1-1-onto𝐵 )

Proof

Step Hyp Ref Expression
1 f1od.1 𝐹 = ( 𝑥𝐴𝐶 )
2 f1od.2 ( ( 𝜑𝑥𝐴 ) → 𝐶𝑊 )
3 f1od.3 ( ( 𝜑𝑦𝐵 ) → 𝐷𝑋 )
4 f1od.4 ( 𝜑 → ( ( 𝑥𝐴𝑦 = 𝐶 ) ↔ ( 𝑦𝐵𝑥 = 𝐷 ) ) )
5 1 2 3 4 f1ocnvd ( 𝜑 → ( 𝐹 : 𝐴1-1-onto𝐵 𝐹 = ( 𝑦𝐵𝐷 ) ) )
6 5 simpld ( 𝜑𝐹 : 𝐴1-1-onto𝐵 )