Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
⊢ ( 𝐵 = 𝐶 → ( 𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) ) |
2 |
1
|
biimpcd |
⊢ ( 𝐵 ∈ 𝐴 → ( 𝐵 = 𝐶 → 𝐶 ∈ 𝐴 ) ) |
3 |
2
|
adantl |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 = 𝐶 → 𝐶 ∈ 𝐴 ) ) |
4 |
|
prcdnq |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ( 𝐶 <Q 𝐵 → 𝐶 ∈ 𝐴 ) ) |
5 |
3 4
|
jaod |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐵 = 𝐶 ∨ 𝐶 <Q 𝐵 ) → 𝐶 ∈ 𝐴 ) ) |
6 |
5
|
con3d |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ( ¬ 𝐶 ∈ 𝐴 → ¬ ( 𝐵 = 𝐶 ∨ 𝐶 <Q 𝐵 ) ) ) |
7 |
6
|
adantr |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 ∈ Q ) → ( ¬ 𝐶 ∈ 𝐴 → ¬ ( 𝐵 = 𝐶 ∨ 𝐶 <Q 𝐵 ) ) ) |
8 |
|
elprnq |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ Q ) |
9 |
|
ltsonq |
⊢ <Q Or Q |
10 |
|
sotric |
⊢ ( ( <Q Or Q ∧ ( 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) ) → ( 𝐵 <Q 𝐶 ↔ ¬ ( 𝐵 = 𝐶 ∨ 𝐶 <Q 𝐵 ) ) ) |
11 |
9 10
|
mpan |
⊢ ( ( 𝐵 ∈ Q ∧ 𝐶 ∈ Q ) → ( 𝐵 <Q 𝐶 ↔ ¬ ( 𝐵 = 𝐶 ∨ 𝐶 <Q 𝐵 ) ) ) |
12 |
8 11
|
sylan |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 ∈ Q ) → ( 𝐵 <Q 𝐶 ↔ ¬ ( 𝐵 = 𝐶 ∨ 𝐶 <Q 𝐵 ) ) ) |
13 |
7 12
|
sylibrd |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 ∈ Q ) → ( ¬ 𝐶 ∈ 𝐴 → 𝐵 <Q 𝐶 ) ) |