Metamath Proof Explorer

Theorem upciclem1

Description: Lemma for upcic , upeu , and upeu2 . (Contributed by Zhi Wang, 16-Sep-2025) (Proof shortened by Zhi Wang, 5-Nov-2025)

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

Proof

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