Metamath Proof Explorer

Theorem genpnnp

Description: The result of an operation on positive reals is different from the set of positive fractions. (Contributed by NM, 29-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 )
genpnnp.3 ⊢ ( 𝑧 ∈ Q → ( 𝑥 <Q 𝑦 ↔ ( 𝑧 𝐺 𝑥 ) <Q ( 𝑧 𝐺 𝑦 ) ) )
genpnnp.4 ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
Assertion genpnnp ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ¬ ( 𝐴 𝐹 𝐵 ) = Q )

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 genpnnp.3 ⊢ ( 𝑧 ∈ Q → ( 𝑥 <Q 𝑦 ↔ ( 𝑧 𝐺 𝑥 ) <Q ( 𝑧 𝐺 𝑦 ) ) )
4 genpnnp.4 ⊢ ( 𝑥 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
5 prpssnq ⊢ ( 𝐴 ∈ P → 𝐴 ⊊ Q )
6 pssnel ⊢ ( 𝐴 ⊊ Q → ∃ 𝑤 ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) )
7 5 6 syl ⊢ ( 𝐴 ∈ P → ∃ 𝑤 ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) )
8 prpssnq ⊢ ( 𝐵 ∈ P → 𝐵 ⊊ Q )
9 pssnel ⊢ ( 𝐵 ⊊ Q → ∃ 𝑣 ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) )
10 8 9 syl ⊢ ( 𝐵 ∈ P → ∃ 𝑣 ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) )
11 7 10 anim12i ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑤 ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) ∧ ∃ 𝑣 ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) ) )
12 exdistrv ⊢ ( ∃ 𝑤 ∃ 𝑣 ( ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) ∧ ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) ) ↔ ( ∃ 𝑤 ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) ∧ ∃ 𝑣 ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) ) )
13 11 12 sylibr ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ∃ 𝑤 ∃ 𝑣 ( ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) ∧ ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) ) )
14 prub ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → ( ¬ 𝑤 ∈ 𝐴 → 𝑓 <Q 𝑤 ) )
15 prub ⊢ ( ( ( 𝐵 ∈ P ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑣 ∈ Q ) → ( ¬ 𝑣 ∈ 𝐵 → 𝑔 <Q 𝑣 ) )
16 14 15 im2anan9 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) ∧ ( ( 𝐵 ∈ P ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑣 ∈ Q ) ) → ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) → ( 𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣 ) ) )
17 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ Q )
18 17 anim1i ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) )
19 elprnq ⊢ ( ( 𝐵 ∈ P ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ Q )
20 19 anim1i ⊢ ( ( ( 𝐵 ∈ P ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑣 ∈ Q ) → ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) )
21 ltsonq ⊢ <Q Or Q
22 so2nr ⊢ ( ( <Q Or Q ∧ ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) ) → ¬ ( 𝑓 <Q 𝑤 ∧ 𝑤 <Q 𝑓 ) )
23 21 22 mpan ⊢ ( ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) → ¬ ( 𝑓 <Q 𝑤 ∧ 𝑤 <Q 𝑓 ) )
24 23 ad2antrr ⊢ ( ( ( ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) ∧ ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) ) ∧ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) → ¬ ( 𝑓 <Q 𝑤 ∧ 𝑤 <Q 𝑓 ) )
25 simpr ⊢ ( ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) → 𝑣 ∈ Q )
26 simpl ⊢ ( ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) → 𝑓 ∈ Q )
27 25 26 anim12i ⊢ ( ( ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) ∧ ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) ) → ( 𝑣 ∈ Q ∧ 𝑓 ∈ Q ) )
28 27 ancoms ⊢ ( ( ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) ∧ ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) ) → ( 𝑣 ∈ Q ∧ 𝑓 ∈ Q ) )
29 vex ⊢ 𝑤 ∈ V
30 vex ⊢ 𝑣 ∈ V
31 vex ⊢ 𝑓 ∈ V
32 vex ⊢ 𝑔 ∈ V
33 29 30 3 31 4 32 caovord3 ⊢ ( ( ( 𝑣 ∈ Q ∧ 𝑓 ∈ Q ) ∧ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) → ( 𝑤 <Q 𝑓 ↔ 𝑔 <Q 𝑣 ) )
34 33 anbi2d ⊢ ( ( ( 𝑣 ∈ Q ∧ 𝑓 ∈ Q ) ∧ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) → ( ( 𝑓 <Q 𝑤 ∧ 𝑤 <Q 𝑓 ) ↔ ( 𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣 ) ) )
35 28 34 sylan ⊢ ( ( ( ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) ∧ ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) ) ∧ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) → ( ( 𝑓 <Q 𝑤 ∧ 𝑤 <Q 𝑓 ) ↔ ( 𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣 ) ) )
36 24 35 mtbid ⊢ ( ( ( ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) ∧ ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) ) ∧ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) → ¬ ( 𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣 ) )
37 36 ex ⊢ ( ( ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) ∧ ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) ) → ( ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) → ¬ ( 𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣 ) ) )
38 37 con2d ⊢ ( ( ( 𝑓 ∈ Q ∧ 𝑤 ∈ Q ) ∧ ( 𝑔 ∈ Q ∧ 𝑣 ∈ Q ) ) → ( ( 𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) )
39 18 20 38 syl2an ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) ∧ ( ( 𝐵 ∈ P ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑣 ∈ Q ) ) → ( ( 𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) )
40 16 39 syld ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) ∧ ( ( 𝐵 ∈ P ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑣 ∈ Q ) ) → ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) )
41 40 an4s ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ 𝑔 ∈ 𝐵 ) ) ∧ ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) ) → ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) )
42 41 ex ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑓 ∈ 𝐴 ) ∧ ( 𝐵 ∈ P ∧ 𝑔 ∈ 𝐵 ) ) → ( ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) → ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) ) )
43 42 an4s ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵 ) ) → ( ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) → ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) ) )
44 43 ex ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) → ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) ) ) )
45 44 com24 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) → ( ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) → ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) ) ) )
46 45 imp32 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) ∧ ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) ) ) → ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵 ) → ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) )
47 46 ralrimivv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) ∧ ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) ) ) → ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐵 ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) )
48 ralnex2 ⊢ ( ∀ 𝑓 ∈ 𝐴 ∀ 𝑔 ∈ 𝐵 ¬ ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ↔ ¬ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) )
49 47 48 sylib ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) ∧ ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) ) ) → ¬ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) )
50 1 2 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) )
51 50 adantr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) ∧ ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) ) ) → ( ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑔 ∈ 𝐵 ( 𝑤 𝐺 𝑣 ) = ( 𝑓 𝐺 𝑔 ) ) )
52 49 51 mtbird ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) ∧ ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) ) ) → ¬ ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) )
53 52 expcom ⊢ ( ( ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) ∧ ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) ) → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ¬ ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )
54 53 ancoms ⊢ ( ( ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) ∧ ( ¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵 ) ) → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ¬ ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )
55 54 an4s ⊢ ( ( ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) ∧ ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) ) → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ¬ ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )
56 2 caovcl ⊢ ( ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) → ( 𝑤 𝐺 𝑣 ) ∈ Q )
57 eleq2 ⊢ ( ( 𝐴 𝐹 𝐵 ) = Q → ( ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) ↔ ( 𝑤 𝐺 𝑣 ) ∈ Q ) )
58 57 biimprcd ⊢ ( ( 𝑤 𝐺 𝑣 ) ∈ Q → ( ( 𝐴 𝐹 𝐵 ) = Q → ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )
59 58 con3d ⊢ ( ( 𝑤 𝐺 𝑣 ) ∈ Q → ( ¬ ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) → ¬ ( 𝐴 𝐹 𝐵 ) = Q ) )
60 56 59 syl ⊢ ( ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) → ( ¬ ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) → ¬ ( 𝐴 𝐹 𝐵 ) = Q ) )
61 60 ad2ant2r ⊢ ( ( ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) ∧ ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) ) → ( ¬ ( 𝑤 𝐺 𝑣 ) ∈ ( 𝐴 𝐹 𝐵 ) → ¬ ( 𝐴 𝐹 𝐵 ) = Q ) )
62 55 61 syldc ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) ∧ ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) ) → ¬ ( 𝐴 𝐹 𝐵 ) = Q ) )
63 62 exlimdvv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑤 ∃ 𝑣 ( ( 𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴 ) ∧ ( 𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵 ) ) → ¬ ( 𝐴 𝐹 𝐵 ) = Q ) )
64 13 63 mpd ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ¬ ( 𝐴 𝐹 𝐵 ) = Q )