Metamath Proof Explorer

Theorem oppcup3lem

Description: Lemma for oppcup3 . (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses oppcup3lem.1 
|- ( ph -> A. y e. B A. n e. ( ( F ` y ) J Z ) E! k e. ( y H X ) n = ( M ( <. ( F ` y ) , ( F ` X ) >. O Z ) ( ( y G X ) ` k ) ) )
oppcup3lem.y 
|- ( ph -> Y e. B )
oppcup3lem.n 
|- ( ph -> N e. ( ( F ` Y ) J Z ) )
Assertion oppcup3lem 
|- ( ph -> E! l e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` l ) ) )

Proof

Step Hyp Ref Expression
1 oppcup3lem.1 
 |-  ( ph -> A. y e. B A. n e. ( ( F ` y ) J Z ) E! k e. ( y H X ) n = ( M ( <. ( F ` y ) , ( F ` X ) >. O Z ) ( ( y G X ) ` k ) ) )
2 oppcup3lem.y 
 |-  ( ph -> Y e. B )
3 oppcup3lem.n 
 |-  ( ph -> N e. ( ( F ` Y ) J Z ) )
4 eqeq1 
 |-  ( n = N -> ( n = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) <-> N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) ) )
5 4 reubidv 
 |-  ( n = N -> ( E! k e. ( Y H X ) n = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) <-> E! k e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) ) )
6 fveq2 
 |-  ( y = Y -> ( F ` y ) = ( F ` Y ) )
7 6 oveq1d 
 |-  ( y = Y -> ( ( F ` y ) J Z ) = ( ( F ` Y ) J Z ) )
8 oveq1 
 |-  ( y = Y -> ( y H X ) = ( Y H X ) )
9 6 opeq1d 
 |-  ( y = Y -> <. ( F ` y ) , ( F ` X ) >. = <. ( F ` Y ) , ( F ` X ) >. )
10 9 oveq1d 
 |-  ( y = Y -> ( <. ( F ` y ) , ( F ` X ) >. O Z ) = ( <. ( F ` Y ) , ( F ` X ) >. O Z ) )
11 eqidd 
 |-  ( y = Y -> M = M )
12 oveq1 
 |-  ( y = Y -> ( y G X ) = ( Y G X ) )
13 12 fveq1d 
 |-  ( y = Y -> ( ( y G X ) ` k ) = ( ( Y G X ) ` k ) )
14 10 11 13 oveq123d 
 |-  ( y = Y -> ( M ( <. ( F ` y ) , ( F ` X ) >. O Z ) ( ( y G X ) ` k ) ) = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) )
15 14 eqeq2d 
 |-  ( y = Y -> ( n = ( M ( <. ( F ` y ) , ( F ` X ) >. O Z ) ( ( y G X ) ` k ) ) <-> n = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) ) )
16 8 15 reueqbidv 
 |-  ( y = Y -> ( E! k e. ( y H X ) n = ( M ( <. ( F ` y ) , ( F ` X ) >. O Z ) ( ( y G X ) ` k ) ) <-> E! k e. ( Y H X ) n = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) ) )
17 7 16 raleqbidv 
 |-  ( y = Y -> ( A. n e. ( ( F ` y ) J Z ) E! k e. ( y H X ) n = ( M ( <. ( F ` y ) , ( F ` X ) >. O Z ) ( ( y G X ) ` k ) ) <-> A. n e. ( ( F ` Y ) J Z ) E! k e. ( Y H X ) n = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) ) )
18 17 1 2 rspcdva 
 |-  ( ph -> A. n e. ( ( F ` Y ) J Z ) E! k e. ( Y H X ) n = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) )
19 5 18 3 rspcdva 
 |-  ( ph -> E! k e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) )
20 fveq2 
 |-  ( k = m -> ( ( Y G X ) ` k ) = ( ( Y G X ) ` m ) )
21 20 oveq2d 
 |-  ( k = m -> ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` m ) ) )
22 21 eqeq2d 
 |-  ( k = m -> ( N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) <-> N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` m ) ) ) )
23 22 cbvreuvw 
 |-  ( E! k e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) <-> E! m e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` m ) ) )
24 fveq2 
 |-  ( m = l -> ( ( Y G X ) ` m ) = ( ( Y G X ) ` l ) )
25 24 oveq2d 
 |-  ( m = l -> ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` m ) ) = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` l ) ) )
26 25 eqeq2d 
 |-  ( m = l -> ( N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` m ) ) <-> N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` l ) ) ) )
27 26 cbvreuvw 
 |-  ( E! m e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` m ) ) <-> E! l e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` l ) ) )
28 23 27 bitri 
 |-  ( E! k e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` k ) ) <-> E! l e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` l ) ) )
29 19 28 sylib 
 |-  ( ph -> E! l e. ( Y H X ) N = ( M ( <. ( F ` Y ) , ( F ` X ) >. O Z ) ( ( Y G X ) ` l ) ) )