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

Metamath Proof Explorer

Theorem f11o

Description: Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998)

		Ref	Expression
	Hypothesis	f11o.1	⊢ 𝐹 ∈ V
	Assertion	f11o	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ∃ 𝑥 ( 𝐹 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		f11o.1	⊢ 𝐹 ∈ V
2	1	ffoss	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
3	2	anbi1i	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ^◡ 𝐹 ) ↔ ( ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ Fun ^◡ 𝐹 ) )
4		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ^◡ 𝐹 ) )
5		dff1o3	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝑥 ↔ ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ Fun ^◡ 𝐹 ) )
6	5	anbi1i	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ Fun ^◡ 𝐹 ) ∧ 𝑥 ⊆ 𝐵 ) )
7		an32	⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ Fun ^◡ 𝐹 ) ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ Fun ^◡ 𝐹 ) )
8	6 7	bitri	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ Fun ^◡ 𝐹 ) )
9	8	exbii	⊢ ( ∃ 𝑥 ( 𝐹 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ∃ 𝑥 ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ Fun ^◡ 𝐹 ) )
10		19.41v	⊢ ( ∃ 𝑥 ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ Fun ^◡ 𝐹 ) ↔ ( ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ Fun ^◡ 𝐹 ) )
11	9 10	bitri	⊢ ( ∃ 𝑥 ( 𝐹 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ Fun ^◡ 𝐹 ) )
12	3 4 11	3bitr4i	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ∃ 𝑥 ( 𝐹 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )