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

Metamath Proof Explorer

Theorem functhinclem2

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

Ref Expression
Hypotheses functhinclem2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
functhinclem2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
functhinclem2.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
Assertion functhinclem2 ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 functhinclem2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
2 functhinclem2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3 functhinclem2.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
4 simpl ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
5 4 fveq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
6 simpr ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
7 6 fveq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
8 5 7 oveq12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
9 8 eqeq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ↔ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ ) )
10 oveq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
11 10 eqeq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( 𝑋 𝐻 𝑌 ) = ∅ ) )
12 9 11 imbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) ↔ ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) ) )
13 12 rspc2gv ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) ) )
14 13 imp ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) ) → ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) )
15 1 2 3 14 syl21anc ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) )