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 ⊢ F Fn X
initopropdlemlem.2 ⊢ φ → ¬ A ∈ Y
initopropdlemlem.3 ⊢ X ⊆ Y
initopropdlemlem.4 ⊢ φ ∧ B ∈ X → F ⁡ B = ∅
Assertion initopropdlemlem ⊢ φ → F ⁡ A = F ⁡ B

Proof

Step Hyp Ref Expression
1 initopropdlemlem.1 ⊢ F Fn X
2 initopropdlemlem.2 ⊢ φ → ¬ A ∈ Y
3 initopropdlemlem.3 ⊢ X ⊆ Y
4 initopropdlemlem.4 ⊢ φ ∧ B ∈ X → F ⁡ B = ∅
5 3 sseli ⊢ A ∈ X → A ∈ Y
6 2 5 nsyl ⊢ φ → ¬ A ∈ X
7 1 fndmi ⊢ dom ⁡ F = X
8 7 eleq2i ⊢ A ∈ dom ⁡ F ↔ A ∈ X
9 ndmfv ⊢ ¬ A ∈ dom ⁡ F → F ⁡ A = ∅
10 8 9 sylnbir ⊢ ¬ A ∈ X → F ⁡ A = ∅
11 6 10 syl ⊢ φ → F ⁡ A = ∅
12 11 adantr ⊢ φ ∧ B ∈ X → F ⁡ A = ∅
13 12 4 eqtr4d ⊢ φ ∧ B ∈ X → F ⁡ A = F ⁡ B
14 11 adantr ⊢ φ ∧ ¬ B ∈ X → F ⁡ A = ∅
15 7 eleq2i ⊢ B ∈ dom ⁡ F ↔ B ∈ X
16 ndmfv ⊢ ¬ B ∈ dom ⁡ F → F ⁡ B = ∅
17 15 16 sylnbir ⊢ ¬ B ∈ X → F ⁡ B = ∅
18 17 adantl ⊢ φ ∧ ¬ B ∈ X → F ⁡ B = ∅
19 14 18 eqtr4d ⊢ φ ∧ ¬ B ∈ X → F ⁡ A = F ⁡ B
20 13 19 pm2.61dan ⊢ φ → F ⁡ A = F ⁡ B