This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )