Theorem iinfssclem2

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	iinfssclem2	|- ( ph -> K Fn ( |^|_ x e. A S X. |^|_ x e. A S ) )

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		ovex	|- ( z H w ) e. _V
7	6	rgenw	|- A. x e. A ( z H w ) e. _V
8		iinexg	|- ( ( A =/= (/) /\ A. x e. A ( z H w ) e. _V ) -> |^|_ x e. A ( z H w ) e. _V )
9	1 7 8	sylancl	|- ( ph -> |^|_ x e. A ( z H w ) e. _V )
10	9	adantr	|- ( ( ph /\ ( z e. |^|_ x e. A S /\ w e. |^|_ x e. A S ) ) -> |^|_ x e. A ( z H w ) e. _V )
11	10	ralrimivva	|- ( ph -> A. z e. |^|_ x e. A S A. w e. |^|_ x e. A S |^|_ x e. A ( z H w ) e. _V )
12		eqid	|- ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) ) = ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) )
13	12	fnmpo	|- ( A. z e. |^|_ x e. A S A. w e. |^|_ x e. A S |^|_ x e. A ( z H w ) e. _V -> ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) ) Fn ( |^|_ x e. A S X. |^|_ x e. A S ) )
14	11 13	syl	|- ( ph -> ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) ) Fn ( |^|_ x e. A S X. |^|_ x e. A S ) )
15	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 ) ) )
16	15	fneq1d	|- ( ph -> ( K Fn ( |^|_ x e. A S X. |^|_ x e. A S ) <-> ( z e. |^|_ x e. A S , w e. |^|_ x e. A S |-> |^|_ x e. A ( z H w ) ) Fn ( |^|_ x e. A S X. |^|_ x e. A S ) ) )
17	14 16	mpbird	|- ( ph -> K Fn ( |^|_ x e. A S X. |^|_ x e. A S ) )