Theorem tgisline

Description: The property of being a proper line, generated by two distinct points. (Contributed by Thierry Arnoux, 25-May-2019)

	Ref	Expression
Hypotheses	tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgisline.1	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
Assertion	tgisline	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tgisline.1	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → 𝐺 ∈ TarskiG )
7		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → 𝑥 ∈ 𝐵 )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) )
9	8	eldifad	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → 𝑦 ∈ 𝐵 )
10		eldifsn	⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 𝑥 ) )
11	8 10	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 𝑥 ) )
12	11	simprd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → 𝑦 ≠ 𝑥 )
13	12	necomd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → 𝑥 ≠ 𝑦 )
14	1 3 2 6 7 9 13	tglngval	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
15	14 13	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) ) → ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) )
16	15	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) )
17	1 3 2	tglng	⊢ ( 𝐺 ∈ TarskiG → 𝐿 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
18	4 17	syl	⊢ ( 𝜑 → 𝐿 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
19	18	rneqd	⊢ ( 𝜑 → ran 𝐿 = ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
20	5 19	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
21		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
22	21	elrnmpog	⊢ ( 𝐴 ∈ ran 𝐿 → ( 𝐴 ∈ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
23	5 22	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
24	20 23	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
25	16 24	r19.29d2r	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
26		difss	⊢ ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝐵
27		simpr	⊢ ( ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
28		simpll	⊢ ( ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
29	27 28	eqtr4d	⊢ ( ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
30		simplr	⊢ ( ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → 𝑥 ≠ 𝑦 )
31	29 30	jca	⊢ ( ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
32	31	reximi	⊢ ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
33		ssrexv	⊢ ( ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝐵 → ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) )
34	26 32 33	mpsyl	⊢ ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → ∃ 𝑦 ∈ 𝐵 ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
35	34	reximi	⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ( ( ( 𝑥 𝐿 𝑦 ) = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ∧ 𝑥 ≠ 𝑦 ) ∧ 𝐴 = { 𝑧 ∈ 𝐵 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
36	25 35	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )