Metamath Proof Explorer

Theorem tglnunirn

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

Ref Expression
Hypotheses tglng.p ⊢ P = Base G
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 = Base G
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 ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
5 4 rneqd ⊢ G ∈ 𝒢 Tarski → ran ⁡ L = ran ⁡ x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
6 5 eleq2d ⊢ G ∈ 𝒢 Tarski → p ∈ ran ⁡ L ↔ p ∈ ran ⁡ x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
7 6 biimpa ⊢ G ∈ 𝒢 Tarski ∧ p ∈ ran ⁡ L → p ∈ ran ⁡ x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
8 eqid ⊢ x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
9 1 fvexi ⊢ P ∈ V
10 9 rabex ⊢ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∈ V
11 8 10 elrnmpo ⊢ p ∈ ran ⁡ x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ↔ ∃ x ∈ P ∃ y ∈ P ∖ x p = z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
12 ssrab2 ⊢ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ⊆ P
13 sseq1 ⊢ p = z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → p ⊆ P ↔ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ⊆ P
14 12 13 mpbiri ⊢ p = z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → p ⊆ P
15 14 rexlimivw ⊢ ∃ y ∈ P ∖ x p = z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → p ⊆ P
16 15 rexlimivw ⊢ ∃ x ∈ P ∃ y ∈ P ∖ x p = z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → p ⊆ P
17 11 16 sylbi ⊢ p ∈ ran ⁡ x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → p ⊆ P
18 7 17 syl ⊢ G ∈ 𝒢 Tarski ∧ p ∈ ran ⁡ L → p ⊆ P
19 18 ralrimiva ⊢ G ∈ 𝒢 Tarski → ∀ p ∈ ran ⁡ L p ⊆ P
20 unissb ⊢ ⋃ ran ⁡ L ⊆ P ↔ ∀ p ∈ ran ⁡ L p ⊆ P
21 19 20 sylibr ⊢ G ∈ 𝒢 Tarski → ⋃ ran ⁡ L ⊆ P