![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tglnpt | Structured version Visualization version Unicode version |
Description: Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019.) |
Ref | Expression |
---|---|
tglng.p |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
tglng.l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
tglng.i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
tglnpt.g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
tglnpt.a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
tglnpt.x |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
tglnpt |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tglnpt.g |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | tglng.p |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | tglng.l |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | tglng.i |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | tglnunirn 24672 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | syl 17 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | tglnpt.a |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | elssuni 4219 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 7, 8 | syl 17 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | tglnpt.x |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | sseldd 3419 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 6, 11 | sseldd 3419 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pr 4639 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-sbc 3256 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-br 4396 df-opab 4455 df-cnv 4847 df-dm 4849 df-rn 4850 df-iota 5553 df-fv 5597 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-trkg 24580 |
This theorem is referenced by: mirln 24800 mirln2 24801 perpcom 24837 perpneq 24838 ragperp 24841 foot 24843 footne 24844 footeq 24845 hlperpnel 24846 perprag 24847 perpdragALT 24848 perpdrag 24849 colperpexlem3 24853 oppne3 24864 oppcom 24865 oppnid 24867 opphllem1 24868 opphllem2 24869 opphllem3 24870 opphllem4 24871 opphllem5 24872 opphllem6 24873 oppperpex 24874 opphl 24875 outpasch 24876 lnopp2hpgb 24884 hpgerlem 24886 colopp 24890 colhp 24891 lmieu 24905 lmimid 24915 lnperpex 24924 trgcopy 24925 trgcopyeulem 24926 |
Copyright terms: Public domain | W3C validator |