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	$⊢ B = {Base}_{G}$
	tglineelsb2.i	$⊢ I = Itv (G)$
	tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
	tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgisline.1	$⊢ φ \to A \in ran L$
Assertion	tgisline	$⊢ φ \to \exists x \in B \exists y \in B (A = x L y \land x \neq y)$

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	$⊢ B = {Base}_{G}$
2		tglineelsb2.i	$⊢ I = Itv (G)$
3		tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgisline.1	$⊢ φ \to A \in ran L$
6	4	adantr	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to G \in 𝒢_{Tarski}$
7		simprl	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to x \in B$
8		simprr	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to y \in (B ∖ \{x\})$
9	8	eldifad	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to y \in B$
10		eldifsn	$⊢ y \in (B ∖ \{x\}) \leftrightarrow (y \in B \land y \neq x)$
11	8 10	sylib	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to (y \in B \land y \neq x)$
12	11	simprd	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to y \neq x$
13	12	necomd	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to x \neq y$
14	1 3 2 6 7 9 13	tglngval	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}$
15	14 13	jca	$⊢ (φ \land (x \in B \land y \in (B ∖ \{x\}))) \to (x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y)$
16	15	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in (B ∖ \{x\}) (x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y)$
17	1 3 2	tglng	$⊢ G \in 𝒢_{Tarski} \to L = (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
18	4 17	syl	$⊢ φ \to L = (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
19	18	rneqd	$⊢ φ \to ran L = ran (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
20	5 19	eleqtrd	$⊢ φ \to A \in ran (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
21		eqid	$⊢ (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) = (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
22	21	elrnmpog	$⊢ A \in ran L \to (A \in ran (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \leftrightarrow \exists x \in B \exists y \in (B ∖ \{x\}) A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
23	5 22	syl	$⊢ φ \to (A \in ran (x \in B, y \in (B ∖ \{x\}) ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \leftrightarrow \exists x \in B \exists y \in (B ∖ \{x\}) A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
24	20 23	mpbid	$⊢ φ \to \exists x \in B \exists y \in (B ∖ \{x\}) A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}$
25	16 24	r19.29d2r	$⊢ φ \to \exists x \in B \exists y \in (B ∖ \{x\}) ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
26		difss	$⊢ B ∖ \{x\} \subseteq B$
27		simpr	$⊢ ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \to A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}$
28		simpll	$⊢ ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \to x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}$
29	27 28	eqtr4d	$⊢ ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \to A = x L y$
30		simplr	$⊢ ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \to x \neq y$
31	29 30	jca	$⊢ ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \to (A = x L y \land x \neq y)$
32	31	reximi	$⊢ \exists y \in (B ∖ \{x\}) ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \to \exists y \in (B ∖ \{x\}) (A = x L y \land x \neq y)$
33		ssrexv	$⊢ B ∖ \{x\} \subseteq B \to (\exists y \in (B ∖ \{x\}) (A = x L y \land x \neq y) \to \exists y \in B (A = x L y \land x \neq y))$
34	26 32 33	mpsyl	$⊢ \exists y \in (B ∖ \{x\}) ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \to \exists y \in B (A = x L y \land x \neq y)$
35	34	reximi	$⊢ \exists x \in B \exists y \in (B ∖ \{x\}) ((x L y = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} \land x \neq y) \land A = \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) \to \exists x \in B \exists y \in B (A = x L y \land x \neq y)$
36	25 35	syl	$⊢ φ \to \exists x \in B \exists y \in B (A = x L y \land x \neq y)$

Metamath Proof Explorer

Theorem tgisline

Proof