Step |
Hyp |
Ref |
Expression |
1 |
|
tglngval.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
tglngval.l |
⊢ 𝐿 = ( LineG ‘ 𝐺 ) |
3 |
|
tglngval.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
|
tglngval.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
5 |
|
tglngval.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑃 ) |
6 |
|
tglngval.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑃 ) |
7 |
|
tgcolg.z |
⊢ ( 𝜑 → 𝑍 ∈ 𝑃 ) |
8 |
|
btwncolg2.z |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ) |
9 |
8
|
3mix2d |
⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) |
10 |
1 2 3 4 5 6 7
|
tgcolg |
⊢ ( 𝜑 → ( ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ↔ ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ∨ 𝑋 ∈ ( 𝑍 𝐼 𝑌 ) ∨ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ) ) |
11 |
9 10
|
mpbird |
⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ∨ 𝑋 = 𝑌 ) ) |