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

Metamath Proof Explorer

Theorem dff1o4

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion dff1o4 ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dff1o2 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) )
2 3anass ⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun ◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ↔ ( 𝐹 Fn 𝐴 ∧ ( Fun ◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ) )
3 df-rn ⊢ ran 𝐹 = dom ◡ 𝐹
4 3 eqeq1i ⊢ ( ran 𝐹 = 𝐵 ↔ dom ◡ 𝐹 = 𝐵 )
5 4 anbi2i ⊢ ( ( Fun ◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ↔ ( Fun ◡ 𝐹 ∧ dom ◡ 𝐹 = 𝐵 ) )
6 df-fn ⊢ ( ◡ 𝐹 Fn 𝐵 ↔ ( Fun ◡ 𝐹 ∧ dom ◡ 𝐹 = 𝐵 ) )
7 5 6 bitr4i ⊢ ( ( Fun ◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ↔ ◡ 𝐹 Fn 𝐵 )
8 7 anbi2i ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( Fun ◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ) ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )
9 1 2 8 3bitri ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐵 ) )