iinfssclem3

Step	Hyp	Ref	Expression
1		iinfssc.1	$⊢ φ \to A \neq \emptyset$
2		iinfssc.2	$⊢ (φ \land x \in A) \to H \subseteq_{cat} J$
3		iinfssc.3	$⊢ φ \to K = (y \in ⋂_{x \in A} dom H ⟼ ⋂_{x \in A} H (y))$
4		iinfssclem1.4	$⊢ (φ \land x \in A) \to S = dom dom H$
5		iinfssclem1.5	$⊢ Ⅎ x φ$
6		iinfssclem3.x	$⊢ φ \to X \in ⋂_{x \in A} S$
7		iinfssclem3.y	$⊢ φ \to Y \in ⋂_{x \in A} S$
8	1 2 3 4 5	iinfssclem1	$⊢ φ \to K = (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w))$
9		nfv	$⊢ Ⅎ x (z = X \land w = Y)$
10	5 9	nfan	$⊢ Ⅎ x (φ \land (z = X \land w = Y))$
11		simplrl	$⊢ ((φ \land (z = X \land w = Y)) \land x \in A) \to z = X$
12		simplrr	$⊢ ((φ \land (z = X \land w = Y)) \land x \in A) \to w = Y$
13	11 12	oveq12d	$⊢ ((φ \land (z = X \land w = Y)) \land x \in A) \to z H w = X H Y$
14	10 13	iineq2d	$⊢ (φ \land (z = X \land w = Y)) \to ⋂_{x \in A} (z H w) = ⋂_{x \in A} (X H Y)$
15		ovex	$⊢ X H Y \in V$
16	15	rgenw	$⊢ \forall x \in A X H Y \in V$
17		iinexg	$⊢ (A \neq \emptyset \land \forall x \in A X H Y \in V) \to ⋂_{x \in A} (X H Y) \in V$
18	1 16 17	sylancl	$⊢ φ \to ⋂_{x \in A} (X H Y) \in V$
19	8 14 6 7 18	ovmpod	$⊢ φ \to X K Y = ⋂_{x \in A} (X H Y)$

Metamath Proof Explorer