This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
Assertion genpn0 ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) )

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 prn0 ⊢ ( 𝐴 ∈ P → 𝐴 ≠ ∅ )
4 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ 𝐴 )
5 3 4 sylib ⊢ ( 𝐴 ∈ P → ∃ 𝑓 𝑓 ∈ 𝐴 )
6 prn0 ⊢ ( 𝐵 ∈ P → 𝐵 ≠ ∅ )
7 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ 𝐵 )
8 6 7 sylib ⊢ ( 𝐵 ∈ P → ∃ 𝑔 𝑔 ∈ 𝐵 )
9 5 8 anim12i ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑓 𝑓 ∈ 𝐴 ∧ ∃ 𝑔 𝑔 ∈ 𝐵 ) )
10 1 2 genpprecl ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑓 𝐺 𝑔 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )
11 ne0i ⊢ ( ( 𝑓 𝐺 𝑔 ) ∈ ( 𝐴 𝐹 𝐵 ) → ( 𝐴 𝐹 𝐵 ) ≠ ∅ )
12 0pss ⊢ ( ∅ ⊊ ( 𝐴 𝐹 𝐵 ) ↔ ( 𝐴 𝐹 𝐵 ) ≠ ∅ )
13 11 12 sylibr ⊢ ( ( 𝑓 𝐺 𝑔 ) ∈ ( 𝐴 𝐹 𝐵 ) → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) )
14 10 13 syl6 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵 ) → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) ) )
15 14 expcomd ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑔 ∈ 𝐵 → ( 𝑓 ∈ 𝐴 → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) ) ) )
16 15 exlimdv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑔 𝑔 ∈ 𝐵 → ( 𝑓 ∈ 𝐴 → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) ) ) )
17 16 com23 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑓 ∈ 𝐴 → ( ∃ 𝑔 𝑔 ∈ 𝐵 → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) ) ) )
18 17 exlimdv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑓 𝑓 ∈ 𝐴 → ( ∃ 𝑔 𝑔 ∈ 𝐵 → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) ) ) )
19 18 impd ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( ∃ 𝑓 𝑓 ∈ 𝐴 ∧ ∃ 𝑔 𝑔 ∈ 𝐵 ) → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) ) )
20 9 19 mpd ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ∅ ⊊ ( 𝐴 𝐹 𝐵 ) )