Theorem f1oresrab

Description: Build a bijection between restricted abstract builders, given a bijection between the base classes, deduction version. (Contributed by Thierry Arnoux, 17-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		f1oresrab.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
2		f1oresrab.2	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
3		f1oresrab.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → ( 𝜒 ↔ 𝜓 ) )
4		f1ofun	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → Fun 𝐹 )
5		funcnvcnv	⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
6	2 4 5	3syl	⊢ ( 𝜑 → Fun ◡ ◡ 𝐹 )
7		f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
8		f1of1	⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐵 –1-1→ 𝐴 )
9	2 7 8	3syl	⊢ ( 𝜑 → ◡ 𝐹 : 𝐵 –1-1→ 𝐴 )
10		ssrab2	⊢ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ⊆ 𝐵
11		f1ores	⊢ ( ( ◡ 𝐹 : 𝐵 –1-1→ 𝐴 ∧ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ⊆ 𝐵 ) → ( ◡ 𝐹 ↾ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) : { 𝑦 ∈ 𝐵 ∣ 𝜒 } –1-1-onto→ ( ◡ 𝐹 “ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) )
12	9 10 11	sylancl	⊢ ( 𝜑 → ( ◡ 𝐹 ↾ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) : { 𝑦 ∈ 𝐵 ∣ 𝜒 } –1-1-onto→ ( ◡ 𝐹 “ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) )
13	1	mptpreima	⊢ ( ◡ 𝐹 “ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) = { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜒 } }
14	3	3expia	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = 𝐶 → ( 𝜒 ↔ 𝜓 ) ) )
15	14	alrimiv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑦 = 𝐶 → ( 𝜒 ↔ 𝜓 ) ) )
16		f1of	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
17	2 16	syl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
18	1	fmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹 : 𝐴 ⟶ 𝐵 )
19	17 18	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 )
20	19	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
21		elrab3t	⊢ ( ( ∀ 𝑦 ( 𝑦 = 𝐶 → ( 𝜒 ↔ 𝜓 ) ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ↔ 𝜓 ) )
22	15 20 21	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ↔ 𝜓 ) )
23	22	rabbidva	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜒 } } = { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
24	13 23	eqtrid	⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) = { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
25	24	f1oeq3d	⊢ ( 𝜑 → ( ( ◡ 𝐹 ↾ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) : { 𝑦 ∈ 𝐵 ∣ 𝜒 } –1-1-onto→ ( ◡ 𝐹 “ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) ↔ ( ◡ 𝐹 ↾ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) : { 𝑦 ∈ 𝐵 ∣ 𝜒 } –1-1-onto→ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) )
26	12 25	mpbid	⊢ ( 𝜑 → ( ◡ 𝐹 ↾ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) : { 𝑦 ∈ 𝐵 ∣ 𝜒 } –1-1-onto→ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
27		f1orescnv	⊢ ( ( Fun ◡ ◡ 𝐹 ∧ ( ◡ 𝐹 ↾ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) : { 𝑦 ∈ 𝐵 ∣ 𝜒 } –1-1-onto→ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) → ( ◡ ◡ 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) : { 𝑥 ∈ 𝐴 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
28	6 26 27	syl2anc	⊢ ( 𝜑 → ( ◡ ◡ 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) : { 𝑥 ∈ 𝐴 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
29		rescnvcnv	⊢ ( ◡ ◡ 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = ( 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )
30		f1oeq1	⊢ ( ( ◡ ◡ 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = ( 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) → ( ( ◡ ◡ 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) : { 𝑥 ∈ 𝐴 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ↔ ( 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) : { 𝑥 ∈ 𝐴 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ) )
31	29 30	ax-mp	⊢ ( ( ◡ ◡ 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) : { 𝑥 ∈ 𝐴 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } ↔ ( 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) : { 𝑥 ∈ 𝐴 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )
32	28 31	sylib	⊢ ( 𝜑 → ( 𝐹 ↾ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) : { 𝑥 ∈ 𝐴 ∣ 𝜓 } –1-1-onto→ { 𝑦 ∈ 𝐵 ∣ 𝜒 } )