Metamath Proof Explorer

Theorem functhinclem2

Description: Lemma for functhinc . (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses functhinclem2.x ⊢ φ → X ∈ B
functhinclem2.y ⊢ φ → Y ∈ B
functhinclem2.1 ⊢ φ → ∀ x ∈ B ∀ y ∈ B F ⁡ x J F ⁡ y = ∅ → x H y = ∅
Assertion functhinclem2 ⊢ φ → F ⁡ X J F ⁡ Y = ∅ → X H Y = ∅

Proof

Step Hyp Ref Expression
1 functhinclem2.x ⊢ φ → X ∈ B
2 functhinclem2.y ⊢ φ → Y ∈ B
3 functhinclem2.1 ⊢ φ → ∀ x ∈ B ∀ y ∈ B F ⁡ x J F ⁡ y = ∅ → x H y = ∅
4 simpl ⊢ x = X ∧ y = Y → x = X
5 4 fveq2d ⊢ x = X ∧ y = Y → F ⁡ x = F ⁡ X
6 simpr ⊢ x = X ∧ y = Y → y = Y
7 6 fveq2d ⊢ x = X ∧ y = Y → F ⁡ y = F ⁡ Y
8 5 7 oveq12d ⊢ x = X ∧ y = Y → F ⁡ x J F ⁡ y = F ⁡ X J F ⁡ Y
9 8 eqeq1d ⊢ x = X ∧ y = Y → F ⁡ x J F ⁡ y = ∅ ↔ F ⁡ X J F ⁡ Y = ∅
10 oveq12 ⊢ x = X ∧ y = Y → x H y = X H Y
11 10 eqeq1d ⊢ x = X ∧ y = Y → x H y = ∅ ↔ X H Y = ∅
12 9 11 imbi12d ⊢ x = X ∧ y = Y → F ⁡ x J F ⁡ y = ∅ → x H y = ∅ ↔ F ⁡ X J F ⁡ Y = ∅ → X H Y = ∅
13 12 rspc2gv ⊢ X ∈ B ∧ Y ∈ B → ∀ x ∈ B ∀ y ∈ B F ⁡ x J F ⁡ y = ∅ → x H y = ∅ → F ⁡ X J F ⁡ Y = ∅ → X H Y = ∅
14 13 imp ⊢ X ∈ B ∧ Y ∈ B ∧ ∀ x ∈ B ∀ y ∈ B F ⁡ x J F ⁡ y = ∅ → x H y = ∅ → F ⁡ X J F ⁡ Y = ∅ → X H Y = ∅
15 1 2 3 14 syl21anc ⊢ φ → F ⁡ X J F ⁡ Y = ∅ → X H Y = ∅