Metamath Proof Explorer

Theorem genpdm

Description: Domain of general operation on positive reals. (Contributed by NM, 18-Nov-1995) (Revised by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	genp.1	$⊢ F = (w \in 𝑷, v \in 𝑷 ⟼ \{x \| \exists y \in w \exists z \in v x = y G z\})$
		genp.2	$⊢ (y \in 𝑸 \land z \in 𝑸) \to y G z \in 𝑸$
	Assertion	genpdm	$⊢ dom F = 𝑷 \times 𝑷$

Proof

Step	Hyp	Ref	Expression
1		genp.1	$⊢ F = (w \in 𝑷, v \in 𝑷 ⟼ \{x \| \exists y \in w \exists z \in v x = y G z\})$
2		genp.2	$⊢ (y \in 𝑸 \land z \in 𝑸) \to y G z \in 𝑸$
3		elprnq	$⊢ (w \in 𝑷 \land y \in w) \to y \in 𝑸$
4		elprnq	$⊢ (v \in 𝑷 \land z \in v) \to z \in 𝑸$
5		eleq1	$⊢ x = y G z \to (x \in 𝑸 \leftrightarrow y G z \in 𝑸)$
6	2 5	syl5ibrcom	$⊢ (y \in 𝑸 \land z \in 𝑸) \to (x = y G z \to x \in 𝑸)$
7	3 4 6	syl2an	$⊢ ((w \in 𝑷 \land y \in w) \land (v \in 𝑷 \land z \in v)) \to (x = y G z \to x \in 𝑸)$
8	7	an4s	$⊢ ((w \in 𝑷 \land v \in 𝑷) \land (y \in w \land z \in v)) \to (x = y G z \to x \in 𝑸)$
9	8	rexlimdvva	$⊢ (w \in 𝑷 \land v \in 𝑷) \to (\exists y \in w \exists z \in v x = y G z \to x \in 𝑸)$
10	9	abssdv	$⊢ (w \in 𝑷 \land v \in 𝑷) \to \{x \| \exists y \in w \exists z \in v x = y G z\} \subseteq 𝑸$
11		nqex	$⊢ 𝑸 \in V$
12		ssexg	$⊢ (\{x \| \exists y \in w \exists z \in v x = y G z\} \subseteq 𝑸 \land 𝑸 \in V) \to \{x \| \exists y \in w \exists z \in v x = y G z\} \in V$
13	10 11 12	sylancl	$⊢ (w \in 𝑷 \land v \in 𝑷) \to \{x \| \exists y \in w \exists z \in v x = y G z\} \in V$
14	13	rgen2	$⊢ \forall w \in 𝑷 \forall v \in 𝑷 \{x \| \exists y \in w \exists z \in v x = y G z\} \in V$
15	1	fnmpo	$⊢ \forall w \in 𝑷 \forall v \in 𝑷 \{x \| \exists y \in w \exists z \in v x = y G z\} \in V \to F Fn (𝑷 \times 𝑷)$
16		fndm	$⊢ F Fn (𝑷 \times 𝑷) \to dom F = 𝑷 \times 𝑷$
17	14 15 16	mp2b	$⊢ dom F = 𝑷 \times 𝑷$