Metamath Proof Explorer

Theorem 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 ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y G z
genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
Assertion genpn0 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → ∅ ⊂ A F B

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ F = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y G z
2 genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
3 prn0 ⊢ A ∈ 𝑷 → A ≠ ∅
4 n0 ⊢ A ≠ ∅ ↔ ∃ f f ∈ A
5 3 4 sylib ⊢ A ∈ 𝑷 → ∃ f f ∈ A
6 prn0 ⊢ B ∈ 𝑷 → B ≠ ∅
7 n0 ⊢ B ≠ ∅ ↔ ∃ g g ∈ B
8 6 7 sylib ⊢ B ∈ 𝑷 → ∃ g g ∈ B
9 5 8 anim12i ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → ∃ f f ∈ A ∧ ∃ g g ∈ B
10 1 2 genpprecl ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → f ∈ A ∧ g ∈ B → f G g ∈ A F B
11 ne0i ⊢ f G g ∈ A F B → A F B ≠ ∅
12 0pss ⊢ ∅ ⊂ A F B ↔ A F B ≠ ∅
13 11 12 sylibr ⊢ f G g ∈ A F B → ∅ ⊂ A F B
14 10 13 syl6 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → f ∈ A ∧ g ∈ B → ∅ ⊂ A F B
15 14 expcomd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → g ∈ B → f ∈ A → ∅ ⊂ A F B
16 15 exlimdv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → ∃ g g ∈ B → f ∈ A → ∅ ⊂ A F B
17 16 com23 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → f ∈ A → ∃ g g ∈ B → ∅ ⊂ A F B
18 17 exlimdv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → ∃ f f ∈ A → ∃ g g ∈ B → ∅ ⊂ A F B
19 18 impd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → ∃ f f ∈ A ∧ ∃ g g ∈ B → ∅ ⊂ A F B
20 9 19 mpd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → ∅ ⊂ A F B