Metamath Proof Explorer

Theorem tglnunirn

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

Ref Expression
Hypotheses tglng.p ⊢P=BaseG
tglng.l ⊢L=Line𝒢⁡G
tglng.i ⊢I=Itv⁡G
Assertion tglnunirn ⊢G∈𝒢Tarski→⋃ran⁡L⊆P

Proof

Step Hyp Ref Expression
1 tglng.p ⊢P=BaseG
2 tglng.l ⊢L=Line𝒢⁡G
3 tglng.i ⊢I=Itv⁡G
4 1 2 3 tglng ⊢G∈𝒢Tarski→L=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
5 4 rneqd ⊢G∈𝒢Tarski→ran⁡L=ran⁡x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
6 5 eleq2d ⊢G∈𝒢Tarski→p∈ran⁡L↔p∈ran⁡x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
7 6 biimpa ⊢G∈𝒢Tarski∧p∈ran⁡L→p∈ran⁡x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
8 eqid ⊢x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
9 1 fvexi ⊢P∈V
10 9 rabex ⊢z∈P|z∈xIy∨x∈zIy∨y∈xIz∈V
11 8 10 elrnmpo ⊢p∈ran⁡x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz↔∃x∈P∃y∈P∖xp=z∈P|z∈xIy∨x∈zIy∨y∈xIz
12 ssrab2 ⊢z∈P|z∈xIy∨x∈zIy∨y∈xIz⊆P
13 sseq1 ⊢p=z∈P|z∈xIy∨x∈zIy∨y∈xIz→p⊆P↔z∈P|z∈xIy∨x∈zIy∨y∈xIz⊆P
14 12 13 mpbiri ⊢p=z∈P|z∈xIy∨x∈zIy∨y∈xIz→p⊆P
15 14 rexlimivw ⊢∃y∈P∖xp=z∈P|z∈xIy∨x∈zIy∨y∈xIz→p⊆P
16 15 rexlimivw ⊢∃x∈P∃y∈P∖xp=z∈P|z∈xIy∨x∈zIy∨y∈xIz→p⊆P
17 11 16 sylbi ⊢p∈ran⁡x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz→p⊆P
18 7 17 syl ⊢G∈𝒢Tarski∧p∈ran⁡L→p⊆P
19 18 ralrimiva ⊢G∈𝒢Tarski→∀p∈ran⁡Lp⊆P
20 unissb ⊢⋃ran⁡L⊆P↔∀p∈ran⁡Lp⊆P
21 19 20 sylibr ⊢G∈𝒢Tarski→⋃ran⁡L⊆P