Step |
Hyp |
Ref |
Expression |
1 |
|
prn0 |
⊢ ( 𝐵 ∈ P → 𝐵 ≠ ∅ ) |
2 |
|
n0 |
⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 ) |
3 |
1 2
|
sylib |
⊢ ( 𝐵 ∈ P → ∃ 𝑦 𝑦 ∈ 𝐵 ) |
4 |
3
|
adantl |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ∃ 𝑦 𝑦 ∈ 𝐵 ) |
5 |
|
addclpr |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) ∈ P ) |
6 |
|
df-plp |
⊢ +P = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 +Q 𝑧 ) } ) |
7 |
|
addclnq |
⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 +Q 𝑧 ) ∈ Q ) |
8 |
6 7
|
genpprecl |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) ) |
9 |
8
|
imp |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) |
10 |
|
elprnq |
⊢ ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) → ( 𝑥 +Q 𝑦 ) ∈ Q ) |
11 |
|
addnqf |
⊢ +Q : ( Q × Q ) ⟶ Q |
12 |
11
|
fdmi |
⊢ dom +Q = ( Q × Q ) |
13 |
|
0nnq |
⊢ ¬ ∅ ∈ Q |
14 |
12 13
|
ndmovrcl |
⊢ ( ( 𝑥 +Q 𝑦 ) ∈ Q → ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) ) |
15 |
|
ltaddnq |
⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → 𝑥 <Q ( 𝑥 +Q 𝑦 ) ) |
16 |
10 14 15
|
3syl |
⊢ ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) → 𝑥 <Q ( 𝑥 +Q 𝑦 ) ) |
17 |
|
prcdnq |
⊢ ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) → ( 𝑥 <Q ( 𝑥 +Q 𝑦 ) → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) ) |
18 |
16 17
|
mpd |
⊢ ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) |
19 |
5 9 18
|
syl2an2r |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) |
20 |
19
|
exp32 |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) ) ) |
21 |
20
|
com23 |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) ) ) |
22 |
21
|
alrimdv |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑦 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) ) ) |
23 |
|
dfss2 |
⊢ ( 𝐴 ⊆ ( 𝐴 +P 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐴 +P 𝐵 ) ) ) |
24 |
22 23
|
syl6ibr |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑦 ∈ 𝐵 → 𝐴 ⊆ ( 𝐴 +P 𝐵 ) ) ) |
25 |
|
vex |
⊢ 𝑦 ∈ V |
26 |
25
|
prlem934 |
⊢ ( 𝐴 ∈ P → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 ) |
27 |
26
|
adantr |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 ) |
28 |
|
eleq2 |
⊢ ( 𝐴 = ( 𝐴 +P 𝐵 ) → ( ( 𝑥 +Q 𝑦 ) ∈ 𝐴 ↔ ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) ) ) |
29 |
28
|
biimprcd |
⊢ ( ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) → ( 𝐴 = ( 𝐴 +P 𝐵 ) → ( 𝑥 +Q 𝑦 ) ∈ 𝐴 ) ) |
30 |
29
|
con3d |
⊢ ( ( 𝑥 +Q 𝑦 ) ∈ ( 𝐴 +P 𝐵 ) → ( ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) |
31 |
8 30
|
syl6 |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) ) |
32 |
31
|
expd |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) ) ) |
33 |
32
|
com34 |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑥 ∈ 𝐴 → ( ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) ) ) |
34 |
33
|
rexlimdv |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝑦 ) ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) ) |
35 |
27 34
|
mpd |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑦 ∈ 𝐵 → ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) |
36 |
24 35
|
jcad |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑦 ∈ 𝐵 → ( 𝐴 ⊆ ( 𝐴 +P 𝐵 ) ∧ ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) ) |
37 |
|
dfpss2 |
⊢ ( 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ↔ ( 𝐴 ⊆ ( 𝐴 +P 𝐵 ) ∧ ¬ 𝐴 = ( 𝐴 +P 𝐵 ) ) ) |
38 |
36 37
|
syl6ibr |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑦 ∈ 𝐵 → 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) ) |
39 |
38
|
exlimdv |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ∃ 𝑦 𝑦 ∈ 𝐵 → 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) ) |
40 |
4 39
|
mpd |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) |
41 |
|
ltprord |
⊢ ( ( 𝐴 ∈ P ∧ ( 𝐴 +P 𝐵 ) ∈ P ) → ( 𝐴 <P ( 𝐴 +P 𝐵 ) ↔ 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) ) |
42 |
5 41
|
syldan |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 <P ( 𝐴 +P 𝐵 ) ↔ 𝐴 ⊊ ( 𝐴 +P 𝐵 ) ) ) |
43 |
40 42
|
mpbird |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → 𝐴 <P ( 𝐴 +P 𝐵 ) ) |