Metamath Proof Explorer

Theorem iinfssclem1

Description: Lemma for iinfssc . (Contributed by Zhi Wang, 31-Oct-2025)

Ref Expression
Hypotheses iinfssc.1 
|- ( ph -> A =/= (/) )
iinfssc.2 
|- ( ( ph /\ x e. A ) -> H C_cat J )
iinfssc.3 
|- ( ph -> K = ( y e. |^|_ x e. A dom H |-> |^|_ x e. A ( H ` y ) ) )
iinfssclem1.4 
|- ( ( ph /\ x e. A ) -> S = dom dom H )
iinfssclem1.5 
|- F/ x ph
Assertion iinfssclem1 
|- ( ph -> K = ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) ) )

Proof

Step Hyp Ref Expression
1 iinfssc.1 
 |-  ( ph -> A =/= (/) )
2 iinfssc.2 
 |-  ( ( ph /\ x e. A ) -> H C_cat J )
3 iinfssc.3 
 |-  ( ph -> K = ( y e. |^|_ x e. A dom H |-> |^|_ x e. A ( H ` y ) ) )
4 iinfssclem1.4 
 |-  ( ( ph /\ x e. A ) -> S = dom dom H )
5 iinfssclem1.5 
 |-  F/ x ph
6 2 4 sscfn1 
 |-  ( ( ph /\ x e. A ) -> H Fn ( S X. S ) )
7 6 fndmd 
 |-  ( ( ph /\ x e. A ) -> dom H = ( S X. S ) )
8 5 7 iineq2d 
 |-  ( ph -> |^|_ x e. A dom H = |^|_ x e. A ( S X. S ) )
9 iinxp 
 |-  ( A =/= (/) -> |^|_ x e. A ( S X. S ) = ( |^|_ x e. A S X. |^|_ x e. A S ) )
10 1 9 syl 
 |-  ( ph -> |^|_ x e. A ( S X. S ) = ( |^|_ x e. A S X. |^|_ x e. A S ) )
11 8 10 eqtrd 
 |-  ( ph -> |^|_ x e. A dom H = ( |^|_ x e. A S X. |^|_ x e. A S ) )
12 11 mpteq1d 
 |-  ( ph -> ( y e. |^|_ x e. A dom H |-> |^|_ x e. A ( H ` y ) ) = ( y e. ( |^|_ x e. A S X. |^|_ x e. A S ) |-> |^|_ x e. A ( H ` y ) ) )
13 3 12 eqtrd 
 |-  ( ph -> K = ( y e. ( |^|_ x e. A S X. |^|_ x e. A S ) |-> |^|_ x e. A ( H ` y ) ) )
14 fveq2 
 |-  ( y = <. z , w >. -> ( H ` y ) = ( H ` <. z , w >. ) )
15 df-ov 
 |-  ( z H w ) = ( H ` <. z , w >. )
16 14 15 eqtr4di 
 |-  ( y = <. z , w >. -> ( H ` y ) = ( z H w ) )
17 16 adantr 
 |-  ( ( y = <. z , w >. /\ x e. A ) -> ( H ` y ) = ( z H w ) )
18 17 iineq2dv 
 |-  ( y = <. z , w >. -> |^|_ x e. A ( H ` y ) = |^|_ x e. A ( z H w ) )
19 18 mpompt 
 |-  ( y e. ( |^|_ x e. A S X. |^|_ x e. A S ) |-> |^|_ x e. A ( H ` y ) ) = ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) )
20 13 19 eqtrdi 
 |-  ( ph -> K = ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) ) )