Step |
Hyp |
Ref |
Expression |
1 |
|
ltexprlem.1 |
⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) } |
2 |
1
|
ltexprlem1 |
⊢ ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → 𝐶 ≠ ∅ ) ) |
3 |
|
0pss |
⊢ ( ∅ ⊊ 𝐶 ↔ 𝐶 ≠ ∅ ) |
4 |
2 3
|
syl6ibr |
⊢ ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → ∅ ⊊ 𝐶 ) ) |
5 |
4
|
imp |
⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → ∅ ⊊ 𝐶 ) |
6 |
1
|
ltexprlem2 |
⊢ ( 𝐵 ∈ P → 𝐶 ⊊ Q ) |
7 |
6
|
adantr |
⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → 𝐶 ⊊ Q ) |
8 |
1
|
ltexprlem3 |
⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ) ) |
9 |
1
|
ltexprlem4 |
⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) ) ) |
10 |
|
df-rex |
⊢ ( ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) ) |
11 |
9 10
|
syl6ibr |
⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) ) |
12 |
8 11
|
jcad |
⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ( ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) ) ) |
13 |
12
|
ralrimiv |
⊢ ( 𝐵 ∈ P → ∀ 𝑥 ∈ 𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → ∀ 𝑥 ∈ 𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) ) |
15 |
|
elnp |
⊢ ( 𝐶 ∈ P ↔ ( ( ∅ ⊊ 𝐶 ∧ 𝐶 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) ) ) |
16 |
5 7 14 15
|
syl21anbrc |
⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → 𝐶 ∈ P ) |