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

Metamath Proof Explorer

Theorem dff1o2

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

		Ref	Expression
	Assertion	dff1o2	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-f1o	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) )
2		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ^◡ 𝐹 ) )
3		df-fo	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) )
4	2 3	anbi12i	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ^◡ 𝐹 ) ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) )
5		anass	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ^◡ 𝐹 ) ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( Fun ^◡ 𝐹 ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) ) )
6		3anan12	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ↔ ( Fun ^◡ 𝐹 ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) )
7	6	anbi1i	⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ↔ ( ( Fun ^◡ 𝐹 ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) )
8		eqimss	⊢ ( ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵 )
9		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
10	9	biimpri	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
11	8 10	sylan2	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
12	11	3adant2	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
13	12	pm4.71i	⊢ ( ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ↔ ( ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) )
14		ancom	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( Fun ^◡ 𝐹 ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) ) ↔ ( ( Fun ^◡ 𝐹 ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) )
15	7 13 14	3bitr4ri	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( Fun ^◡ 𝐹 ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) ) ↔ ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) )
16	5 15	bitri	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ^◡ 𝐹 ) ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) ) ↔ ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) )
17	4 16	bitri	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ↔ ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) )
18	1 17	bitri	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ Fun ^◡ 𝐹 ∧ ran 𝐹 = 𝐵 ) )