Metamath Proof Explorer

Theorem tglnunirn

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

Ref Expression
Hypotheses tglng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglng.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion tglnunirn ( 𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃 )

Proof

Step Hyp Ref Expression
1 tglng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 tglng.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 1 2 3 tglng ⊢ ( 𝐺 ∈ TarskiG → 𝐿 = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
5 4 rneqd ⊢ ( 𝐺 ∈ TarskiG → ran 𝐿 = ran ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
6 5 eleq2d ⊢ ( 𝐺 ∈ TarskiG → ( 𝑝 ∈ ran 𝐿 ↔ 𝑝 ∈ ran ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ) )
7 6 biimpa ⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑝 ∈ ran 𝐿 ) → 𝑝 ∈ ran ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
8 eqid ⊢ ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
9 1 fvexi ⊢ 𝑃 ∈ V
10 9 rabex ⊢ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∈ V
11 8 10 elrnmpo ⊢ ( 𝑝 ∈ ran ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) 𝑝 = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
12 ssrab2 ⊢ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ⊆ 𝑃
13 sseq1 ⊢ ( 𝑝 = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } → ( 𝑝 ⊆ 𝑃 ↔ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ⊆ 𝑃 ) )
14 12 13 mpbiri ⊢ ( 𝑝 = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } → 𝑝 ⊆ 𝑃 )
15 14 rexlimivw ⊢ ( ∃ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) 𝑝 = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } → 𝑝 ⊆ 𝑃 )
16 15 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) 𝑝 = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } → 𝑝 ⊆ 𝑃 )
17 11 16 sylbi ⊢ ( 𝑝 ∈ ran ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → 𝑝 ⊆ 𝑃 )
18 7 17 syl ⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑝 ∈ ran 𝐿 ) → 𝑝 ⊆ 𝑃 )
19 18 ralrimiva ⊢ ( 𝐺 ∈ TarskiG → ∀ 𝑝 ∈ ran 𝐿 𝑝 ⊆ 𝑃 )
20 unissb ⊢ ( ∪ ran 𝐿 ⊆ 𝑃 ↔ ∀ 𝑝 ∈ ran 𝐿 𝑝 ⊆ 𝑃 )
21 19 20 sylibr ⊢ ( 𝐺 ∈ TarskiG → ∪ ran 𝐿 ⊆ 𝑃 )