Theorem initopropdlemlem

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

	Ref	Expression
Hypotheses	initopropdlemlem.1	$$⊢FFnX$$
	initopropdlemlem.2	$$⊢\phi \to \neg A\in Y$$
	initopropdlemlem.3	$$⊢X\subseteq Y$$
	initopropdlemlem.4	$$⊢\left(\phi \wedge B\in X\right)\to F\left(B\right)=\varnothing$$
Assertion	initopropdlemlem	$$⊢\phi \to F\left(A\right)=F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		initopropdlemlem.1	$$⊢FFnX$$
2		initopropdlemlem.2	$$⊢\phi \to \neg A\in Y$$
3		initopropdlemlem.3	$$⊢X\subseteq Y$$
4		initopropdlemlem.4	$$⊢\left(\phi \wedge B\in X\right)\to F\left(B\right)=\varnothing$$
5	3	sseli	$$⊢A\in X\to A\in Y$$
6	2 5	nsyl	$$⊢\phi \to \neg A\in X$$
7	1	fndmi	$$⊢\mathrm{dom}F=X$$
8	7	eleq2i	$$⊢A\in \mathrm{dom}F\leftrightarrow A\in X$$
9		ndmfv	$$⊢\neg A\in \mathrm{dom}F\to F\left(A\right)=\varnothing$$
10	8 9	sylnbir	$$⊢\neg A\in X\to F\left(A\right)=\varnothing$$
11	6 10	syl	$$⊢\phi \to F\left(A\right)=\varnothing$$
12	11	adantr	$$⊢\left(\phi \wedge B\in X\right)\to F\left(A\right)=\varnothing$$
13	12 4	eqtr4d	$$⊢\left(\phi \wedge B\in X\right)\to F\left(A\right)=F\left(B\right)$$
14	11	adantr	$$⊢\left(\phi \wedge \neg B\in X\right)\to F\left(A\right)=\varnothing$$
15	7	eleq2i	$$⊢B\in \mathrm{dom}F\leftrightarrow B\in X$$
16		ndmfv	$$⊢\neg B\in \mathrm{dom}F\to F\left(B\right)=\varnothing$$
17	15 16	sylnbir	$$⊢\neg B\in X\to F\left(B\right)=\varnothing$$
18	17	adantl	$$⊢\left(\phi \wedge \neg B\in X\right)\to F\left(B\right)=\varnothing$$
19	14 18	eqtr4d	$$⊢\left(\phi \wedge \neg B\in X\right)\to F\left(A\right)=F\left(B\right)$$
20	13 19	pm2.61dan	$$⊢\phi \to F\left(A\right)=F\left(B\right)$$