Metamath Proof Explorer


Theorem tglnfn

Description: Lines as functions. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglng.p 𝑃 = ( Base ‘ 𝐺 )
tglng.l 𝐿 = ( LineG ‘ 𝐺 )
tglng.i 𝐼 = ( Itv ‘ 𝐺 )
Assertion tglnfn ( 𝐺 ∈ TarskiG → 𝐿 Fn ( ( 𝑃 × 𝑃 ) ∖ I ) )

Proof

Step Hyp Ref Expression
1 tglng.p 𝑃 = ( Base ‘ 𝐺 )
2 tglng.l 𝐿 = ( LineG ‘ 𝐺 )
3 tglng.i 𝐼 = ( Itv ‘ 𝐺 )
4 1 fvexi 𝑃 ∈ V
5 4 rabex { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∈ V
6 5 rgen2w 𝑥𝑃𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∈ V
7 eqid ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
8 7 fmpox ( ∀ 𝑥𝑃𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∈ V ↔ ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) : 𝑥𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ⟶ V )
9 6 8 mpbi ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) : 𝑥𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ⟶ V
10 ffn ( ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) : 𝑥𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ⟶ V → ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn 𝑥𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) )
11 9 10 ax-mp ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn 𝑥𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) )
12 xpdifid 𝑥𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) = ( ( 𝑃 × 𝑃 ) ∖ I )
13 12 fneq2i ( ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn 𝑥𝑃 ( { 𝑥 } × ( 𝑃 ∖ { 𝑥 } ) ) ↔ ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ( ( 𝑃 × 𝑃 ) ∖ I ) )
14 11 13 mpbi ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ( ( 𝑃 × 𝑃 ) ∖ I )
15 1 2 3 tglng ( 𝐺 ∈ TarskiG → 𝐿 = ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
16 15 fneq1d ( 𝐺 ∈ TarskiG → ( 𝐿 Fn ( ( 𝑃 × 𝑃 ) ∖ I ) ↔ ( 𝑥𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) Fn ( ( 𝑃 × 𝑃 ) ∖ I ) ) )
17 14 16 mpbiri ( 𝐺 ∈ TarskiG → 𝐿 Fn ( ( 𝑃 × 𝑃 ) ∖ I ) )