Step |
Hyp |
Ref |
Expression |
1 |
|
cvbr |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) ) |
2 |
|
psseq2 |
⊢ ( 𝑥 = 𝐶 → ( 𝐴 ⊊ 𝑥 ↔ 𝐴 ⊊ 𝐶 ) ) |
3 |
|
psseq1 |
⊢ ( 𝑥 = 𝐶 → ( 𝑥 ⊊ 𝐵 ↔ 𝐶 ⊊ 𝐵 ) ) |
4 |
2 3
|
anbi12d |
⊢ ( 𝑥 = 𝐶 → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ↔ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) ) |
5 |
4
|
rspcev |
⊢ ( ( 𝐶 ∈ Cℋ ∧ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) |
6 |
5
|
ex |
⊢ ( 𝐶 ∈ Cℋ → ( ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) → ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) |
7 |
6
|
con3rr3 |
⊢ ( ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) → ( 𝐶 ∈ Cℋ → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) → ( 𝐶 ∈ Cℋ → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) ) |
9 |
1 8
|
syl6bi |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ( 𝐶 ∈ Cℋ → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) ) ) |
10 |
9
|
com23 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐶 ∈ Cℋ → ( 𝐴 ⋖ℋ 𝐵 → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) ) ) |
11 |
10
|
3impia |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ¬ ( 𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵 ) ) ) |