Theorem f1oresf1orab

Description: Build a bijection by restricting the domain of a bijection. (Contributed by AV, 1-Aug-2022)

	Ref	Expression
Hypotheses	f1oresf1orab.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	f1oresf1orab.2	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
	f1oresf1orab.3	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
	f1oresf1orab.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → ( 𝜒 ↔ 𝑥 ∈ 𝐷 ) )
Assertion	f1oresf1orab	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )

Proof

Step	Hyp	Ref	Expression
1		f1oresf1orab.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2		f1oresf1orab.2	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
3		f1oresf1orab.3	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
4		f1oresf1orab.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → ( 𝜒 ↔ 𝑥 ∈ 𝐷 ) )
5	1 2 4	f1oresrab	⊢ ( 𝜑 → ( 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐷 } ) : { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐷 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
6		dfss7	⊢ ( 𝐷 ⊆ 𝐴 ↔ { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐷 } = 𝐷 )
7	3 6	sylib	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐷 } = 𝐷 )
8	7	eqcomd	⊢ ( 𝜑 → 𝐷 = { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐷 } )
9	8	reseq2d	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) = ( 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐷 } ) )
10		eqidd	⊢ ( 𝜑 → { 𝑦 ∈ 𝐵 ∣ 𝜒 } = { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
11	9 8 10	f1oeq123d	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ↔ ( 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐷 } ) : { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐷 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) )
12	5 11	mpbird	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )