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	⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = ∅ → ( 𝑋 𝐻 𝑌 ) = ∅ ) )