Metamath Proof Explorer

Theorem upciclem1

Description: Lemma for upcic , upeu , and upeu2 . (Contributed by Zhi Wang, 16-Sep-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 6 oveq2d 
 |-  ( y = Y -> ( <. Z , ( F ` X ) >. O ( F ` y ) ) = ( <. Z , ( F ` X ) >. O ( F ` Y ) ) )
9 oveq2 
 |-  ( y = Y -> ( X G y ) = ( X G Y ) )
10 9 fveq1d 
 |-  ( y = Y -> ( ( X G y ) ` k ) = ( ( X G Y ) ` k ) )
11 eqidd 
 |-  ( y = Y -> M = M )
12 8 10 11 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 ) )
13 12 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 ) ) )
14 13 reubidv 
 |-  ( 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 ) ) )
15 oveq2 
 |-  ( y = Y -> ( X H y ) = ( X H Y ) )
16 15 reueqdv 
 |-  ( 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 ) ) )
17 14 16 bitrd 
 |-  ( 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 ) ) )
18 7 17 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 ) ) )
19 18 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 ) )
20 5 19 3 rspcdva 
 |-  ( ph -> E! k e. ( X H Y ) N = ( ( ( X G Y ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
21 fveq2 
 |-  ( k = m -> ( ( X G Y ) ` k ) = ( ( X G Y ) ` m ) )
22 21 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 ) )
23 22 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 ) ) )
24 23 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 ) )
25 fveq2 
 |-  ( m = l -> ( ( X G Y ) ` m ) = ( ( X G Y ) ` l ) )
26 25 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 ) )
27 26 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 ) ) )
28 27 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 ) )
29 24 28 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 ) )
30 20 29 sylib 
 |-  ( ph -> E! l e. ( X H Y ) N = ( ( ( X G Y ) ` l ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )