Theorem f1ossf1o

Description: Restricting a bijection, which is a mapping from a restricted class abstraction, to a subset is a bijection. (Contributed by AV, 7-Aug-2022)

	Ref	Expression
Hypotheses	f1ossf1o.x	⊢ 𝑋 = { 𝑤 ∈ 𝐴 ∣ ( 𝜓 ∧ 𝜒 ) }
	f1ossf1o.y	⊢ 𝑌 = { 𝑤 ∈ 𝐴 ∣ 𝜓 }
	f1ossf1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
	f1ossf1o.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑌 ↦ 𝐵 )
	f1ossf1o.b	⊢ ( 𝜑 → 𝐺 : 𝑌 –1-1-onto→ 𝐶 )
	f1ossf1o.s	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 = 𝐵 ) → ( 𝜏 ↔ [ 𝑥 / 𝑤 ] 𝜒 ) )
Assertion	f1ossf1o	⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ { 𝑦 ∈ 𝐶 ∣ 𝜏 } )

Proof

Step	Hyp	Ref	Expression
1		f1ossf1o.x	⊢ 𝑋 = { 𝑤 ∈ 𝐴 ∣ ( 𝜓 ∧ 𝜒 ) }
2		f1ossf1o.y	⊢ 𝑌 = { 𝑤 ∈ 𝐴 ∣ 𝜓 }
3		f1ossf1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ 𝐵 )
4		f1ossf1o.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑌 ↦ 𝐵 )
5		f1ossf1o.b	⊢ ( 𝜑 → 𝐺 : 𝑌 –1-1-onto→ 𝐶 )
6		f1ossf1o.s	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ∧ 𝑦 = 𝐵 ) → ( 𝜏 ↔ [ 𝑥 / 𝑤 ] 𝜒 ) )
7	4 5 6	f1oresrab	⊢ ( 𝜑 → ( 𝐺 ↾ { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } ) : { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } –1-1-onto→ { 𝑦 ∈ 𝐶 ∣ 𝜏 } )
8		simpl	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜓 )
9	8	a1i	⊢ ( 𝑤 ∈ 𝐴 → ( ( 𝜓 ∧ 𝜒 ) → 𝜓 ) )
10	9	ss2rabi	⊢ { 𝑤 ∈ 𝐴 ∣ ( 𝜓 ∧ 𝜒 ) } ⊆ { 𝑤 ∈ 𝐴 ∣ 𝜓 }
11	10 1 2	3sstr4i	⊢ 𝑋 ⊆ 𝑌
12	11	a1i	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
13	12	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
14	4	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) )
15	2	rabeqi	⊢ { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } = { 𝑥 ∈ { 𝑤 ∈ 𝐴 ∣ 𝜓 } ∣ [ 𝑥 / 𝑤 ] 𝜒 }
16		nfcv	⊢ Ⅎ 𝑤 𝑥
17		nfcv	⊢ Ⅎ 𝑤 𝐴
18		nfs1v	⊢ Ⅎ 𝑤 [ 𝑥 / 𝑤 ] 𝜓
19		sbequ12	⊢ ( 𝑤 = 𝑥 → ( 𝜓 ↔ [ 𝑥 / 𝑤 ] 𝜓 ) )
20	16 17 18 19	elrabf	⊢ ( 𝑥 ∈ { 𝑤 ∈ 𝐴 ∣ 𝜓 } ↔ ( 𝑥 ∈ 𝐴 ∧ [ 𝑥 / 𝑤 ] 𝜓 ) )
21	20	anbi1i	⊢ ( ( 𝑥 ∈ { 𝑤 ∈ 𝐴 ∣ 𝜓 } ∧ [ 𝑥 / 𝑤 ] 𝜒 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ [ 𝑥 / 𝑤 ] 𝜓 ) ∧ [ 𝑥 / 𝑤 ] 𝜒 ) )
22		anass	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ [ 𝑥 / 𝑤 ] 𝜓 ) ∧ [ 𝑥 / 𝑤 ] 𝜒 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( [ 𝑥 / 𝑤 ] 𝜓 ∧ [ 𝑥 / 𝑤 ] 𝜒 ) ) )
23	21 22	bitri	⊢ ( ( 𝑥 ∈ { 𝑤 ∈ 𝐴 ∣ 𝜓 } ∧ [ 𝑥 / 𝑤 ] 𝜒 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( [ 𝑥 / 𝑤 ] 𝜓 ∧ [ 𝑥 / 𝑤 ] 𝜒 ) ) )
24	23	rabbia2	⊢ { 𝑥 ∈ { 𝑤 ∈ 𝐴 ∣ 𝜓 } ∣ [ 𝑥 / 𝑤 ] 𝜒 } = { 𝑥 ∈ 𝐴 ∣ ( [ 𝑥 / 𝑤 ] 𝜓 ∧ [ 𝑥 / 𝑤 ] 𝜒 ) }
25		nfcv	⊢ Ⅎ 𝑥 𝐴
26		nfv	⊢ Ⅎ 𝑥 ( 𝜓 ∧ 𝜒 )
27		nfs1v	⊢ Ⅎ 𝑤 [ 𝑥 / 𝑤 ] 𝜒
28	18 27	nfan	⊢ Ⅎ 𝑤 ( [ 𝑥 / 𝑤 ] 𝜓 ∧ [ 𝑥 / 𝑤 ] 𝜒 )
29		sbequ12	⊢ ( 𝑤 = 𝑥 → ( 𝜒 ↔ [ 𝑥 / 𝑤 ] 𝜒 ) )
30	19 29	anbi12d	⊢ ( 𝑤 = 𝑥 → ( ( 𝜓 ∧ 𝜒 ) ↔ ( [ 𝑥 / 𝑤 ] 𝜓 ∧ [ 𝑥 / 𝑤 ] 𝜒 ) ) )
31	17 25 26 28 30	cbvrabw	⊢ { 𝑤 ∈ 𝐴 ∣ ( 𝜓 ∧ 𝜒 ) } = { 𝑥 ∈ 𝐴 ∣ ( [ 𝑥 / 𝑤 ] 𝜓 ∧ [ 𝑥 / 𝑤 ] 𝜒 ) }
32	1 31	eqtr2i	⊢ { 𝑥 ∈ 𝐴 ∣ ( [ 𝑥 / 𝑤 ] 𝜓 ∧ [ 𝑥 / 𝑤 ] 𝜒 ) } = 𝑋
33	15 24 32	3eqtri	⊢ { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } = 𝑋
34	33	a1i	⊢ ( 𝜑 → { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } = 𝑋 )
35	14 34	reseq12d	⊢ ( 𝜑 → ( 𝐺 ↾ { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } ) = ( ( 𝑥 ∈ 𝑌 ↦ 𝐵 ) ↾ 𝑋 ) )
36	3	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
37	13 35 36	3eqtr4rd	⊢ ( 𝜑 → 𝐹 = ( 𝐺 ↾ { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } ) )
38	15 24	eqtr2i	⊢ { 𝑥 ∈ 𝐴 ∣ ( [ 𝑥 / 𝑤 ] 𝜓 ∧ [ 𝑥 / 𝑤 ] 𝜒 ) } = { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 }
39	1 31 38	3eqtri	⊢ 𝑋 = { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 }
40	39	a1i	⊢ ( 𝜑 → 𝑋 = { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } )
41		eqidd	⊢ ( 𝜑 → { 𝑦 ∈ 𝐶 ∣ 𝜏 } = { 𝑦 ∈ 𝐶 ∣ 𝜏 } )
42	37 40 41	f1oeq123d	⊢ ( 𝜑 → ( 𝐹 : 𝑋 –1-1-onto→ { 𝑦 ∈ 𝐶 ∣ 𝜏 } ↔ ( 𝐺 ↾ { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } ) : { 𝑥 ∈ 𝑌 ∣ [ 𝑥 / 𝑤 ] 𝜒 } –1-1-onto→ { 𝑦 ∈ 𝐶 ∣ 𝜏 } ) )
43	7 42	mpbird	⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ { 𝑦 ∈ 𝐶 ∣ 𝜏 } )