Theorem initopropdlemlem

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

	Ref	Expression
Hypotheses	initopropdlemlem.1	⊢ 𝐹 Fn 𝑋
	initopropdlemlem.2	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝑌 )
	initopropdlemlem.3	⊢ 𝑋 ⊆ 𝑌
	initopropdlemlem.4	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) = ∅ )
Assertion	initopropdlemlem	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		initopropdlemlem.1	⊢ 𝐹 Fn 𝑋
2		initopropdlemlem.2	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝑌 )
3		initopropdlemlem.3	⊢ 𝑋 ⊆ 𝑌
4		initopropdlemlem.4	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) = ∅ )
5	3	sseli	⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ 𝑌 )
6	2 5	nsyl	⊢ ( 𝜑 → ¬ 𝐴 ∈ 𝑋 )
7	1	fndmi	⊢ dom 𝐹 = 𝑋
8	7	eleq2i	⊢ ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ 𝑋 )
9		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
10	8 9	sylnbir	⊢ ( ¬ 𝐴 ∈ 𝑋 → ( 𝐹 ‘ 𝐴 ) = ∅ )
11	6 10	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ∅ )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
13	12 4	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )
14	11	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
15	7	eleq2i	⊢ ( 𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝑋 )
16		ndmfv	⊢ ( ¬ 𝐵 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐵 ) = ∅ )
17	15 16	sylnbir	⊢ ( ¬ 𝐵 ∈ 𝑋 → ( 𝐹 ‘ 𝐵 ) = ∅ )
18	17	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐵 ) = ∅ )
19	14 18	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )
20	13 19	pm2.61dan	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )