Theorem initopropdlemlem

Description: Lemma for initopropdlem , termopropdlem , and zeroopropdlem . (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Hypotheses	initopropdlemlem.1	|- F Fn X
	initopropdlemlem.2	|- ( ph -> -. A e. Y )
	initopropdlemlem.3	|- X C_ Y
	initopropdlemlem.4	|- ( ( ph /\ B e. X ) -> ( F ` B ) = (/) )
Assertion	initopropdlemlem	|- ( ph -> ( F ` A ) = ( F ` B ) )

Proof

Step	Hyp	Ref	Expression
1		initopropdlemlem.1	|- F Fn X
2		initopropdlemlem.2	|- ( ph -> -. A e. Y )
3		initopropdlemlem.3	|- X C_ Y
4		initopropdlemlem.4	|- ( ( ph /\ B e. X ) -> ( F ` B ) = (/) )
5	3	sseli	|- ( A e. X -> A e. Y )
6	2 5	nsyl	|- ( ph -> -. A e. X )
7	1	fndmi	|- dom F = X
8	7	eleq2i	|- ( A e. dom F <-> A e. X )
9		ndmfv	|- ( -. A e. dom F -> ( F ` A ) = (/) )
10	8 9	sylnbir	|- ( -. A e. X -> ( F ` A ) = (/) )
11	6 10	syl	|- ( ph -> ( F ` A ) = (/) )
12	11	adantr	|- ( ( ph /\ B e. X ) -> ( F ` A ) = (/) )
13	12 4	eqtr4d	|- ( ( ph /\ B e. X ) -> ( F ` A ) = ( F ` B ) )
14	11	adantr	|- ( ( ph /\ -. B e. X ) -> ( F ` A ) = (/) )
15	7	eleq2i	|- ( B e. dom F <-> B e. X )
16		ndmfv	|- ( -. B e. dom F -> ( F ` B ) = (/) )
17	15 16	sylnbir	|- ( -. B e. X -> ( F ` B ) = (/) )
18	17	adantl	|- ( ( ph /\ -. B e. X ) -> ( F ` B ) = (/) )
19	14 18	eqtr4d	|- ( ( ph /\ -. B e. X ) -> ( F ` A ) = ( F ` B ) )
20	13 19	pm2.61dan	|- ( ph -> ( F ` A ) = ( F ` B ) )