genpn0

Description: The result of an operation on positive reals is not empty. (Contributed by NM, 28-Feb-1996) (Revised by Mario Carneiro, 12-Jun-2013) (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	genpn0	$⊢ (A \in 𝑷 \land B \in 𝑷) \to \emptyset \subset A F B$

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		prn0	$⊢ A \in 𝑷 \to A \neq \emptyset$
4		n0	$⊢ A \neq \emptyset \leftrightarrow \exists f f \in A$
5	3 4	sylib	$⊢ A \in 𝑷 \to \exists f f \in A$
6		prn0	$⊢ B \in 𝑷 \to B \neq \emptyset$
7		n0	$⊢ B \neq \emptyset \leftrightarrow \exists g g \in B$
8	6 7	sylib	$⊢ B \in 𝑷 \to \exists g g \in B$
9	5 8	anim12i	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists f f \in A \land \exists g g \in B)$
10	1 2	genpprecl	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((f \in A \land g \in B) \to f G g \in (A F B))$
11		ne0i	$⊢ f G g \in (A F B) \to A F B \neq \emptyset$
12		0pss	$⊢ \emptyset \subset A F B \leftrightarrow A F B \neq \emptyset$
13	11 12	sylibr	$⊢ f G g \in (A F B) \to \emptyset \subset A F B$
14	10 13	syl6	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((f \in A \land g \in B) \to \emptyset \subset A F B)$
15	14	expcomd	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (g \in B \to (f \in A \to \emptyset \subset A F B))$
16	15	exlimdv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists g g \in B \to (f \in A \to \emptyset \subset A F B))$
17	16	com23	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (f \in A \to (\exists g g \in B \to \emptyset \subset A F B))$
18	17	exlimdv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists f f \in A \to (\exists g g \in B \to \emptyset \subset A F B))$
19	18	impd	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((\exists f f \in A \land \exists g g \in B) \to \emptyset \subset A F B)$
20	9 19	mpd	$⊢ (A \in 𝑷 \land B \in 𝑷) \to \emptyset \subset A F B$

Metamath Proof Explorer

Theorem genpn0

Proof