![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tglnpt | Structured version Visualization version GIF version |
Description: Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019.) |
Ref | Expression |
---|---|
tglng.p | ⊢ 𝑃 = (Base‘𝐺) |
tglng.l | ⊢ 𝐿 = (LineG‘𝐺) |
tglng.i | ⊢ 𝐼 = (Itv‘𝐺) |
tglnpt.g | ⊢ (𝜑 → 𝐺 ∈ TarskiG) |
tglnpt.a | ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |
tglnpt.x | ⊢ (𝜑 → 𝑋 ∈ 𝐴) |
Ref | Expression |
---|---|
tglnpt | ⊢ (𝜑 → 𝑋 ∈ 𝑃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tglnpt.g | . . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiG) | |
2 | tglng.p | . . . 4 ⊢ 𝑃 = (Base‘𝐺) | |
3 | tglng.l | . . . 4 ⊢ 𝐿 = (LineG‘𝐺) | |
4 | tglng.i | . . . 4 ⊢ 𝐼 = (Itv‘𝐺) | |
5 | 2, 3, 4 | tglnunirn 25859 | . . 3 ⊢ (𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃) |
6 | 1, 5 | syl 17 | . 2 ⊢ (𝜑 → ∪ ran 𝐿 ⊆ 𝑃) |
7 | tglnpt.a | . . . 4 ⊢ (𝜑 → 𝐴 ∈ ran 𝐿) | |
8 | elssuni 4688 | . . . 4 ⊢ (𝐴 ∈ ran 𝐿 → 𝐴 ⊆ ∪ ran 𝐿) | |
9 | 7, 8 | syl 17 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ ∪ ran 𝐿) |
10 | tglnpt.x | . . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐴) | |
11 | 9, 10 | sseldd 3827 | . 2 ⊢ (𝜑 → 𝑋 ∈ ∪ ran 𝐿) |
12 | 6, 11 | sseldd 3827 | 1 ⊢ (𝜑 → 𝑋 ∈ 𝑃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ∈ wcel 2166 ⊆ wss 3797 ∪ cuni 4657 ran crn 5342 ‘cfv 6122 Basecbs 16221 TarskiGcstrkg 25741 Itvcitv 25747 LineGclng 25748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pr 5126 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-opab 4935 df-cnv 5349 df-dm 5351 df-rn 5352 df-iota 6085 df-fv 6130 df-ov 6907 df-oprab 6908 df-mpt2 6909 df-trkg 25764 |
This theorem is referenced by: mirln 25987 mirln2 25988 perpcom 26024 perpneq 26025 ragperp 26028 foot 26030 footne 26031 footeq 26032 hlperpnel 26033 perprag 26034 perpdragALT 26035 perpdrag 26036 colperpexlem3 26040 oppne3 26051 oppcom 26052 oppnid 26054 opphllem1 26055 opphllem2 26056 opphllem3 26057 opphllem4 26058 opphllem5 26059 opphllem6 26060 oppperpex 26061 opphl 26062 outpasch 26063 lnopp2hpgb 26071 hpgerlem 26073 colopp 26077 colhp 26078 lmieu 26092 lmimid 26102 lnperpex 26111 trgcopy 26112 trgcopyeulem 26113 |
Copyright terms: Public domain | W3C validator |