Theorem smfpimcclem

Description: Lemma for smfpimcc given the choice function C . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smfpimcclem.n	⊢ Ⅎ 𝑛 𝜑
	smfpimcclem.z	⊢ 𝑍 ∈ 𝑉
	smfpimcclem.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	smfpimcclem.c	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) → ( 𝐶 ‘ 𝑦 ) ∈ 𝑦 )
	smfpimcclem.h	⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
Assertion	smfpimcclem	⊢ ( 𝜑 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimcclem.n	⊢ Ⅎ 𝑛 𝜑
2		smfpimcclem.z	⊢ 𝑍 ∈ 𝑉
3		smfpimcclem.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
4		smfpimcclem.c	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) → ( 𝐶 ‘ 𝑦 ) ∈ 𝑦 )
5		smfpimcclem.h	⊢ 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
6		ssrab2	⊢ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ⊆ 𝑆
7		eqid	⊢ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) }
8	7 3	rabexd	⊢ ( 𝜑 → { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ V )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ V )
10		simpl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
12		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) = ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } )
13	12	elrnmpt1	⊢ ( ( 𝑛 ∈ 𝑍 ∧ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ V ) → { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
14	11 9 13	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
15	10 14	jca	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝜑 ∧ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) )
16		eleq1	⊢ ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } → ( 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ↔ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) )
17	16	anbi2d	⊢ ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } → ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) ↔ ( 𝜑 ∧ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) ) )
18		fveq2	⊢ ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } → ( 𝐶 ‘ 𝑦 ) = ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
19		id	⊢ ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } → 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } )
20	18 19	eleq12d	⊢ ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } → ( ( 𝐶 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
21	17 20	imbi12d	⊢ ( 𝑦 = { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } → ( ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) → ( 𝐶 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ( ( 𝜑 ∧ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) → ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) )
22	21 4	vtoclg	⊢ ( { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ V → ( ( 𝜑 ∧ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ∈ ran ( 𝑛 ∈ 𝑍 ↦ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) → ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
23	9 15 22	sylc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } )
24	6 23	sselid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ 𝑆 )
25	1 24 5	fmptdf	⊢ ( 𝜑 → 𝐻 : 𝑍 ⟶ 𝑆 )
26		nfcv	⊢ Ⅎ 𝑠 𝐶
27		nfrab1	⊢ Ⅎ 𝑠 { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) }
28	26 27	nffv	⊢ Ⅎ 𝑠 ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } )
29		nfcv	⊢ Ⅎ 𝑠 𝑆
30		nfcv	⊢ Ⅎ 𝑠 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 )
31		nfcv	⊢ Ⅎ 𝑠 dom ( 𝐹 ‘ 𝑛 )
32	28 31	nfin	⊢ Ⅎ 𝑠 ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∩ dom ( 𝐹 ‘ 𝑛 ) )
33	30 32	nfeq	⊢ Ⅎ 𝑠 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∩ dom ( 𝐹 ‘ 𝑛 ) )
34		ineq1	⊢ ( 𝑠 = ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) → ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
35	34	eqeq2d	⊢ ( 𝑠 = ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) → ( ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) ↔ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
36	28 29 33 35	elrabf	⊢ ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ↔ ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ 𝑆 ∧ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
37	23 36	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ 𝑆 ∧ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
38	37	simprd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
39	5	a1i	⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ 𝑍 ↦ ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) )
40	23	elexd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∈ V )
41	39 40	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
42	41	ineq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
43	38 42	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
44	43	ex	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
45	1 44	ralrimi	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
46	2	elexi	⊢ 𝑍 ∈ V
47	46	mptex	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) ) ∈ V
48	5 47	eqeltri	⊢ 𝐻 ∈ V
49		feq1	⊢ ( ℎ = 𝐻 → ( ℎ : 𝑍 ⟶ 𝑆 ↔ 𝐻 : 𝑍 ⟶ 𝑆 ) )
50		nfcv	⊢ Ⅎ 𝑛 ℎ
51		nfmpt1	⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑍 ↦ ( 𝐶 ‘ { 𝑠 ∈ 𝑆 ∣ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( 𝑠 ∩ dom ( 𝐹 ‘ 𝑛 ) ) } ) )
52	5 51	nfcxfr	⊢ Ⅎ 𝑛 𝐻
53	50 52	nfeq	⊢ Ⅎ 𝑛 ℎ = 𝐻
54		fveq1	⊢ ( ℎ = 𝐻 → ( ℎ ‘ 𝑛 ) = ( 𝐻 ‘ 𝑛 ) )
55	54	ineq1d	⊢ ( ℎ = 𝐻 → ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) )
56	55	eqeq2d	⊢ ( ℎ = 𝐻 → ( ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ↔ ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
57	53 56	ralbid	⊢ ( ℎ = 𝐻 → ( ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
58	49 57	anbi12d	⊢ ( ℎ = 𝐻 → ( ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝐻 : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) ) )
59	48 58	spcev	⊢ ( ( 𝐻 : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( 𝐻 ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )
60	25 45 59	syl2anc	⊢ ( 𝜑 → ∃ ℎ ( ℎ : 𝑍 ⟶ 𝑆 ∧ ∀ 𝑛 ∈ 𝑍 ( ◡ ( 𝐹 ‘ 𝑛 ) “ 𝐴 ) = ( ( ℎ ‘ 𝑛 ) ∩ dom ( 𝐹 ‘ 𝑛 ) ) ) )