Metamath Proof Explorer


Theorem tglnpt

Description: Lines are sets of points. (Contributed by Thierry Arnoux, 17-Oct-2019)

Ref Expression
Hypotheses tglng.p P=BaseG
tglng.l L=Line𝒢G
tglng.i I=ItvG
tglnpt.g φG𝒢Tarski
tglnpt.a φAranL
tglnpt.x φXA
Assertion tglnpt φXP

Proof

Step Hyp Ref Expression
1 tglng.p P=BaseG
2 tglng.l L=Line𝒢G
3 tglng.i I=ItvG
4 tglnpt.g φG𝒢Tarski
5 tglnpt.a φAranL
6 tglnpt.x φXA
7 1 2 3 tglnunirn G𝒢TarskiranLP
8 4 7 syl φranLP
9 elssuni AranLAranL
10 5 9 syl φAranL
11 10 6 sseldd φXranL
12 8 11 sseldd φXP