Metamath Proof Explorer

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 ⊢ B = Base G
tglineelsb2.i ⊢ I = Itv ⁡ G
tglineelsb2.l ⊢ L = Line 𝒢 ⁡ G
tglineelsb2.g ⊢ φ → G ∈ 𝒢 Tarski
tgisline.1 ⊢ φ → A ∈ ran ⁡ L
Assertion tgisline ⊢ φ → ∃ x ∈ B ∃ y ∈ B A = x L y ∧ x ≠ 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 ⊢ φ → G ∈ 𝒢 Tarski
5 tgisline.1 ⊢ φ → A ∈ ran ⁡ L
6 4 adantr ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → G ∈ 𝒢 Tarski
7 simprl ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → x ∈ B
8 simprr ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → y ∈ B ∖ x
9 8 eldifad ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → y ∈ B
10 eldifsn ⊢ y ∈ B ∖ x ↔ y ∈ B ∧ y ≠ x
11 8 10 sylib ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → y ∈ B ∧ y ≠ x
12 11 simprd ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → y ≠ x
13 12 necomd ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → x ≠ y
14 1 3 2 6 7 9 13 tglngval ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
15 14 13 jca ⊢ φ ∧ x ∈ B ∧ y ∈ B ∖ x → x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y
16 15 ralrimivva ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∖ x x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y
17 1 3 2 tglng ⊢ G ∈ 𝒢 Tarski → L = x ∈ B , y ∈ B ∖ x ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
18 4 17 syl ⊢ φ → L = x ∈ B , y ∈ B ∖ x ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
19 18 rneqd ⊢ φ → ran ⁡ L = ran ⁡ x ∈ B , y ∈ B ∖ x ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
20 5 19 eleqtrd ⊢ φ → A ∈ ran ⁡ x ∈ B , y ∈ B ∖ x ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
21 eqid ⊢ x ∈ B , y ∈ B ∖ x ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z = x ∈ B , y ∈ B ∖ x ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
22 21 elrnmpog ⊢ A ∈ ran ⁡ L → A ∈ ran ⁡ x ∈ B , y ∈ B ∖ x ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ↔ ∃ x ∈ B ∃ y ∈ B ∖ x A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
23 5 22 syl ⊢ φ → A ∈ ran ⁡ x ∈ B , y ∈ B ∖ x ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ↔ ∃ x ∈ B ∃ y ∈ B ∖ x A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
24 20 23 mpbid ⊢ φ → ∃ x ∈ B ∃ y ∈ B ∖ x A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
25 16 24 r19.29d2r ⊢ φ → ∃ x ∈ B ∃ y ∈ B ∖ x x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
26 difss ⊢ B ∖ x ⊆ B
27 simpr ⊢ x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
28 simpll ⊢ x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
29 27 28 eqtr4d ⊢ x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → A = x L y
30 simplr ⊢ x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → x ≠ y
31 29 30 jca ⊢ x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → A = x L y ∧ x ≠ y
32 31 reximi ⊢ ∃ y ∈ B ∖ x x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → ∃ y ∈ B ∖ x A = x L y ∧ x ≠ y
33 ssrexv ⊢ B ∖ x ⊆ B → ∃ y ∈ B ∖ x A = x L y ∧ x ≠ y → ∃ y ∈ B A = x L y ∧ x ≠ y
34 26 32 33 mpsyl ⊢ ∃ y ∈ B ∖ x x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → ∃ y ∈ B A = x L y ∧ x ≠ y
35 34 reximi ⊢ ∃ x ∈ B ∃ y ∈ B ∖ x x L y = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ x ≠ y ∧ A = z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z → ∃ x ∈ B ∃ y ∈ B A = x L y ∧ x ≠ y
36 25 35 syl ⊢ φ → ∃ x ∈ B ∃ y ∈ B A = x L y ∧ x ≠ y