Theorem iinfssclem3

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
	iinfssclem3.x	|- ( ph -> X e. |^|_ x e. A S )
	iinfssclem3.y	|- ( ph -> Y e. |^|_ x e. A S )
Assertion	iinfssclem3	|- ( ph -> ( X K Y ) = |^|_ x e. A ( X H Y ) )

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		iinfssclem3.x	|- ( ph -> X e. |^|_ x e. A S )
7		iinfssclem3.y	|- ( ph -> Y e. |^|_ x e. A S )
8	1 2 3 4 5	iinfssclem1	|- ( ph -> K = ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) ) )
9		nfv	|- F/ x ( z = X /\ w = Y )
10	5 9	nfan	|- F/ x ( ph /\ ( z = X /\ w = Y ) )
11		simplrl	|- ( ( ( ph /\ ( z = X /\ w = Y ) ) /\ x e. A ) -> z = X )
12		simplrr	|- ( ( ( ph /\ ( z = X /\ w = Y ) ) /\ x e. A ) -> w = Y )
13	11 12	oveq12d	|- ( ( ( ph /\ ( z = X /\ w = Y ) ) /\ x e. A ) -> ( z H w ) = ( X H Y ) )
14	10 13	iineq2d	|- ( ( ph /\ ( z = X /\ w = Y ) ) -> |^|_ x e. A ( z H w ) = |^|_ x e. A ( X H Y ) )
15		ovex	|- ( X H Y ) e. _V
16	15	rgenw	|- A. x e. A ( X H Y ) e. _V
17		iinexg	|- ( ( A =/= (/) /\ A. x e. A ( X H Y ) e. _V ) -> |^|_ x e. A ( X H Y ) e. _V )
18	1 16 17	sylancl	|- ( ph -> |^|_ x e. A ( X H Y ) e. _V )
19	8 14 6 7 18	ovmpod	|- ( ph -> ( X K Y ) = |^|_ x e. A ( X H Y ) )