Theorem fint

Description: Function into an intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Hypothesis	fint.1	⊢ 𝐵 ≠ ∅
Assertion	fint	⊢ ( 𝐹 : 𝐴 ⟶ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐹 : 𝐴 ⟶ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		fint.1	⊢ 𝐵 ≠ ∅
2		ssint	⊢ ( ran 𝐹 ⊆ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ran 𝐹 ⊆ 𝑥 )
3	2	anbi2i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ∩ 𝐵 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ran 𝐹 ⊆ 𝑥 ) )
4		r19.28zv	⊢ ( 𝐵 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ran 𝐹 ⊆ 𝑥 ) ) )
5	1 4	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ran 𝐹 ⊆ 𝑥 ) )
6	3 5	bitr4i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ∩ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) )
7		df-f	⊢ ( 𝐹 : 𝐴 ⟶ ∩ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ∩ 𝐵 ) )
8		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝑥 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) )
9	8	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐵 𝐹 : 𝐴 ⟶ 𝑥 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) )
10	6 7 9	3bitr4i	⊢ ( 𝐹 : 𝐴 ⟶ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐹 : 𝐴 ⟶ 𝑥 )