riinint

Description: Express a relative indexed intersection as an intersection. (Contributed by Stefan O'Rear, 22-Feb-2015)

		Ref	Expression
	Assertion	riinint	$⊢ (X \in V \land \forall k \in I S \subseteq X) \to X \cap ⋂_{k \in I} S = ⋂ (\{X\} \cup ran (k \in I ⟼ S))$

Step	Hyp	Ref	Expression
1		ssexg	$⊢ (S \subseteq X \land X \in V) \to S \in V$
2	1	expcom	$⊢ X \in V \to (S \subseteq X \to S \in V)$
3	2	ralimdv	$⊢ X \in V \to (\forall k \in I S \subseteq X \to \forall k \in I S \in V)$
4	3	imp	$⊢ (X \in V \land \forall k \in I S \subseteq X) \to \forall k \in I S \in V$
5		dfiin3g	$⊢ \forall k \in I S \in V \to ⋂_{k \in I} S = ⋂ ran (k \in I ⟼ S)$
6	4 5	syl	$⊢ (X \in V \land \forall k \in I S \subseteq X) \to ⋂_{k \in I} S = ⋂ ran (k \in I ⟼ S)$
7	6	ineq2d	$⊢ (X \in V \land \forall k \in I S \subseteq X) \to X \cap ⋂_{k \in I} S = X \cap ⋂ ran (k \in I ⟼ S)$
8		intun	$⊢ ⋂ (\{X\} \cup ran (k \in I ⟼ S)) = ⋂ \{X\} \cap ⋂ ran (k \in I ⟼ S)$
9		intsng	$⊢ X \in V \to ⋂ \{X\} = X$
10	9	adantr	$⊢ (X \in V \land \forall k \in I S \subseteq X) \to ⋂ \{X\} = X$
11	10	ineq1d	$⊢ (X \in V \land \forall k \in I S \subseteq X) \to ⋂ \{X\} \cap ⋂ ran (k \in I ⟼ S) = X \cap ⋂ ran (k \in I ⟼ S)$
12	8 11	eqtrid	$⊢ (X \in V \land \forall k \in I S \subseteq X) \to ⋂ (\{X\} \cup ran (k \in I ⟼ S)) = X \cap ⋂ ran (k \in I ⟼ S)$
13	7 12	eqtr4d	$⊢ (X \in V \land \forall k \in I S \subseteq X) \to X \cap ⋂_{k \in I} S = ⋂ (\{X\} \cup ran (k \in I ⟼ S))$

Metamath Proof Explorer