Metamath Proof Explorer

Theorem iinfssclem2

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

		Ref	Expression
	Hypotheses	iinfssc.1	$⊢ φ \to A \neq \emptyset$
		iinfssc.2	$⊢ (φ \land x \in A) \to H \subseteq_{cat} J$
		iinfssc.3	$⊢ φ \to K = (y \in ⋂_{x \in A} dom H ⟼ ⋂_{x \in A} H (y))$
		iinfssclem1.4	$⊢ (φ \land x \in A) \to S = dom dom H$
		iinfssclem1.5	$⊢ Ⅎ x φ$
	Assertion	iinfssclem2	$⊢ φ \to K Fn (⋂_{x \in A} S \times ⋂_{x \in A} S)$

Proof

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		ovex	$⊢ z H w \in V$
7	6	rgenw	$⊢ \forall x \in A z H w \in V$
8		iinexg	$⊢ (A \neq \emptyset \land \forall x \in A z H w \in V) \to ⋂_{x \in A} (z H w) \in V$
9	1 7 8	sylancl	$⊢ φ \to ⋂_{x \in A} (z H w) \in V$
10	9	adantr	$⊢ (φ \land (z \in ⋂_{x \in A} S \land w \in ⋂_{x \in A} S)) \to ⋂_{x \in A} (z H w) \in V$
11	10	ralrimivva	$⊢ φ \to \forall z \in ⋂_{x \in A} S \forall w \in ⋂_{x \in A} S ⋂_{x \in A} (z H w) \in V$
12		eqid	$⊢ (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w)) = (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w))$
13	12	fnmpo	$⊢ \forall z \in ⋂_{x \in A} S \forall w \in ⋂_{x \in A} S ⋂_{x \in A} (z H w) \in V \to (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w)) Fn (⋂_{x \in A} S \times ⋂_{x \in A} S)$
14	11 13	syl	$⊢ φ \to (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w)) Fn (⋂_{x \in A} S \times ⋂_{x \in A} S)$
15	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))$
16	15	fneq1d	$⊢ φ \to (K Fn (⋂_{x \in A} S \times ⋂_{x \in A} S) \leftrightarrow (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w)) Fn (⋂_{x \in A} S \times ⋂_{x \in A} S))$
17	14 16	mpbird	$⊢ φ \to K Fn (⋂_{x \in A} S \times ⋂_{x \in A} S)$