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 ) )