Metamath Proof Explorer

Theorem mpoexxg2

Description: Existence of an operation class abstraction (version for dependent domains, i.e. the first base class may depend on the second base class), analogous to mpoexxg . (Contributed by AV, 30-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		mpoexxg2.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2	1	mpofun	$⊢ Fun F$
3	1	dmmpossx2	$⊢ dom F \subseteq ⋃_{y \in B} (A \times \{y\})$
4		vsnex	$⊢ \{y\} \in V$
5		xpexg	$⊢ (A \in S \land \{y\} \in V) \to A \times \{y\} \in V$
6	4 5	mpan2	$⊢ A \in S \to A \times \{y\} \in V$
7	6	ralimi	$⊢ \forall y \in B A \in S \to \forall y \in B A \times \{y\} \in V$
8		iunexg	$⊢ (B \in R \land \forall y \in B A \times \{y\} \in V) \to ⋃_{y \in B} (A \times \{y\}) \in V$
9	7 8	sylan2	$⊢ (B \in R \land \forall y \in B A \in S) \to ⋃_{y \in B} (A \times \{y\}) \in V$
10		ssexg	$⊢ (dom F \subseteq ⋃_{y \in B} (A \times \{y\}) \land ⋃_{y \in B} (A \times \{y\}) \in V) \to dom F \in V$
11	3 9 10	sylancr	$⊢ (B \in R \land \forall y \in B A \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	$⊢ (B \in R \land \forall y \in B A \in S) \to F \in V$