iinfssclem1

	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	iinfssclem1	$⊢ φ \to K = (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w))$

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	2 4	sscfn1	$⊢ (φ \land x \in A) \to H Fn (S \times S)$
7	6	fndmd	$⊢ (φ \land x \in A) \to dom H = S \times S$
8	5 7	iineq2d	$⊢ φ \to ⋂_{x \in A} dom H = ⋂_{x \in A} (S \times S)$
9		iinxp	$⊢ A \neq \emptyset \to ⋂_{x \in A} (S \times S) = ⋂_{x \in A} S \times ⋂_{x \in A} S$
10	1 9	syl	$⊢ φ \to ⋂_{x \in A} (S \times S) = ⋂_{x \in A} S \times ⋂_{x \in A} S$
11	8 10	eqtrd	$⊢ φ \to ⋂_{x \in A} dom H = ⋂_{x \in A} S \times ⋂_{x \in A} S$
12	11	mpteq1d	$⊢ φ \to (y \in ⋂_{x \in A} dom H ⟼ ⋂_{x \in A} H (y)) = (y \in (⋂_{x \in A} S \times ⋂_{x \in A} S) ⟼ ⋂_{x \in A} H (y))$
13	3 12	eqtrd	$⊢ φ \to K = (y \in (⋂_{x \in A} S \times ⋂_{x \in A} S) ⟼ ⋂_{x \in A} H (y))$
14		fveq2	$⊢ y = ⟨z, w⟩ \to H (y) = H (⟨z, w⟩)$
15		df-ov	$⊢ z H w = H (⟨z, w⟩)$
16	14 15	eqtr4di	$⊢ y = ⟨z, w⟩ \to H (y) = z H w$
17	16	adantr	$⊢ (y = ⟨z, w⟩ \land x \in A) \to H (y) = z H w$
18	17	iineq2dv	$⊢ y = ⟨z, w⟩ \to ⋂_{x \in A} H (y) = ⋂_{x \in A} (z H w)$
19	18	mpompt	$⊢ (y \in (⋂_{x \in A} S \times ⋂_{x \in A} S) ⟼ ⋂_{x \in A} H (y)) = (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w))$
20	13 19	eqtrdi	$⊢ φ \to K = (z \in ⋂_{x \in A} S, w \in ⋂_{x \in A} S ⟼ ⋂_{x \in A} (z H w))$

Metamath Proof Explorer

Theorem iinfssclem1

Proof