Theorem functhinclem2

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

	Ref	Expression
Hypotheses	functhinclem2.x	|- ( ph -> X e. B )
	functhinclem2.y	|- ( ph -> Y e. B )
	functhinclem2.1	|- ( ph -> A. x e. B A. y e. B ( ( ( F ` x ) J ( F ` y ) ) = (/) -> ( x H y ) = (/) ) )
Assertion	functhinclem2	|- ( ph -> ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		functhinclem2.x	|- ( ph -> X e. B )
2		functhinclem2.y	|- ( ph -> Y e. B )
3		functhinclem2.1	|- ( ph -> A. x e. B A. y e. 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 e. B /\ Y e. B ) -> ( A. x e. B A. y e. B ( ( ( F ` x ) J ( F ` y ) ) = (/) -> ( x H y ) = (/) ) -> ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) ) )
14	13	imp	|- ( ( ( X e. B /\ Y e. B ) /\ A. x e. B A. y e. B ( ( ( F ` x ) J ( F ` y ) ) = (/) -> ( x H y ) = (/) ) ) -> ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) )
15	1 2 3 14	syl21anc	|- ( ph -> ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) )