mpoexxg

Description: Existence of an operation class abstraction (version for dependent domains). (Contributed by Mario Carneiro, 30-Dec-2016)

		Ref	Expression
	Hypothesis	mpoexg.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	mpoexxg	$⊢ (A \in R \land \forall x \in A B \in S) \to F \in V$

Step	Hyp	Ref	Expression
1		mpoexg.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2	1	mpofun	$⊢ Fun F$
3	1	dmmpossx	$⊢ dom F \subseteq ⋃_{x \in A} (\{x\} \times B)$
4		vsnex	$⊢ \{x\} \in V$
5		xpexg	$⊢ (\{x\} \in V \land B \in S) \to \{x\} \times B \in V$
6	4 5	mpan	$⊢ B \in S \to \{x\} \times B \in V$
7	6	ralimi	$⊢ \forall x \in A B \in S \to \forall x \in A \{x\} \times B \in V$
8		iunexg	$⊢ (A \in R \land \forall x \in A \{x\} \times B \in V) \to ⋃_{x \in A} (\{x\} \times B) \in V$
9	7 8	sylan2	$⊢ (A \in R \land \forall x \in A B \in S) \to ⋃_{x \in A} (\{x\} \times B) \in V$
10		ssexg	$⊢ (dom F \subseteq ⋃_{x \in A} (\{x\} \times B) \land ⋃_{x \in A} (\{x\} \times B) \in V) \to dom F \in V$
11	3 9 10	sylancr	$⊢ (A \in R \land \forall x \in A B \in S) \to dom F \in V$
12		funex	$⊢ (Fun F \land dom F \in V) \to F \in V$
13	2 11 12	sylancr	$⊢ (A \in R \land \forall x \in A B \in S) \to F \in V$

Metamath Proof Explorer