Theorem bj-gabima

Description: Generalized class abstraction as a direct image.

TODO: improve the support lemmas elimag and fvelima to nonfreeness hypothesis (and for the latter, biconditional). (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Hypotheses	bj-gabima.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	bj-gabima.nff	⊢ ( 𝜑 → Ⅎ 𝑥 𝐹 )
	bj-gabima.fun	⊢ ( 𝜑 → Fun 𝐹 )
	bj-gabima.dm	⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ dom 𝐹 )
Assertion	bj-gabima	⊢ ( 𝜑 → { ( 𝐹 ‘ 𝑥 ) ∣ 𝑥 ∣ 𝜓 } = ( 𝐹 “ { 𝑥 ∣ 𝜓 } ) )

Proof

Step	Hyp	Ref	Expression
1		bj-gabima.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		bj-gabima.nff	⊢ ( 𝜑 → Ⅎ 𝑥 𝐹 )
3		bj-gabima.fun	⊢ ( 𝜑 → Fun 𝐹 )
4		bj-gabima.dm	⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } ⊆ dom 𝐹 )
5		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 )
6		vex	⊢ 𝑦 ∈ V
7	6	a1i	⊢ ( 𝜑 → 𝑦 ∈ V )
8		df-rex	⊢ ( ∃ 𝑧 ∈ { 𝑥 ∣ 𝜓 } ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
9	8	a1i	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ { 𝑥 ∣ 𝜓 } ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
10		eqcom	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑧 ) = 𝑦 )
11		df-clab	⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑧 / 𝑥 ] 𝜓 )
12	11	bicomi	⊢ ( [ 𝑧 / 𝑥 ] 𝜓 ↔ 𝑧 ∈ { 𝑥 ∣ 𝜓 } )
13	10 12	anbi12ci	⊢ ( ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ↔ ( 𝑧 ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
14	13	exbii	⊢ ( ∃ 𝑧 ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ↔ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
15	14	a1i	⊢ ( 𝜑 → ( ∃ 𝑧 ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ↔ ∃ 𝑧 ( 𝑧 ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
16	1	nf5i	⊢ Ⅎ 𝑥 𝜑
17		nfcv	⊢ Ⅎ 𝑥 𝑦
18	17	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 )
19		nfcv	⊢ Ⅎ 𝑥 𝑧
20	19	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 )
21	2 20	nffvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) )
22	18 21	nfeqd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 = ( 𝐹 ‘ 𝑧 ) )
23		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜓
24	23	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜓 )
25	22 24	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ∧ [ 𝑧 / 𝑥 ] 𝜓 ) )
26		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
27	26	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
28		sbequ12r	⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑥 ] 𝜓 ↔ 𝜓 ) )
29	27 28	anbi12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ↔ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝜓 ) ) )
30	29	a1i	⊢ ( 𝜑 → ( 𝑧 = 𝑥 → ( ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ↔ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝜓 ) ) ) )
31	16 25 30	cbvexdw	⊢ ( 𝜑 → ( ∃ 𝑧 ( 𝑦 = ( 𝐹 ‘ 𝑧 ) ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ↔ ∃ 𝑥 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝜓 ) ) )
32	9 15 31	3bitr2rd	⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝜓 ) ↔ ∃ 𝑧 ∈ { 𝑥 ∣ 𝜓 } ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
33	1 5 7 32	bj-elgab	⊢ ( 𝜑 → ( 𝑦 ∈ { ( 𝐹 ‘ 𝑥 ) ∣ 𝑥 ∣ 𝜓 } ↔ ∃ 𝑧 ∈ { 𝑥 ∣ 𝜓 } ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
34	3	funfnd	⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
35	34 4	fvelimabd	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐹 “ { 𝑥 ∣ 𝜓 } ) ↔ ∃ 𝑧 ∈ { 𝑥 ∣ 𝜓 } ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
36	33 35	bitr4d	⊢ ( 𝜑 → ( 𝑦 ∈ { ( 𝐹 ‘ 𝑥 ) ∣ 𝑥 ∣ 𝜓 } ↔ 𝑦 ∈ ( 𝐹 “ { 𝑥 ∣ 𝜓 } ) ) )
37	36	eqrdv	⊢ ( 𝜑 → { ( 𝐹 ‘ 𝑥 ) ∣ 𝑥 ∣ 𝜓 } = ( 𝐹 “ { 𝑥 ∣ 𝜓 } ) )