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 
|- ( 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 ) = (/) ) )