Theorem f1oresf1o

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

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

Proof

Step	Hyp	Ref	Expression
1		f1oresf1o.1	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
2		f1oresf1o.2	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
3		f1oresf1o.3	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜒 ) ) )
4		f1of1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 )
5	1 4	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )
6		f1ores	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐷 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( 𝐹 “ 𝐷 ) )
7	5 2 6	syl2anc	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( 𝐹 “ 𝐷 ) )
8		f1ofun	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → Fun 𝐹 )
9	1 8	syl	⊢ ( 𝜑 → Fun 𝐹 )
10		f1odm	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → dom 𝐹 = 𝐴 )
11	1 10	syl	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
12	2 11	sseqtrrd	⊢ ( 𝜑 → 𝐷 ⊆ dom 𝐹 )
13		dfimafn	⊢ ( ( Fun 𝐹 ∧ 𝐷 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐷 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
14	9 12 13	syl2anc	⊢ ( 𝜑 → ( 𝐹 “ 𝐷 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
15	3	abbidv	⊢ ( 𝜑 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜒 ) } )
16		df-rab	⊢ { 𝑦 ∈ 𝐵 ∣ 𝜒 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜒 ) }
17	15 16	eqtr4di	⊢ ( 𝜑 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝑥 ) = 𝑦 } = { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
18	14 17	eqtr2d	⊢ ( 𝜑 → { 𝑦 ∈ 𝐵 ∣ 𝜒 } = ( 𝐹 “ 𝐷 ) )
19	18	f1oeq3d	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ↔ ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ ( 𝐹 “ 𝐷 ) ) )
20	7 19	mpbird	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐷 ) : 𝐷 –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )