This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isline

Description: The predicate "is a line". (Contributed by NM, 19-Sep-2011)

Ref Expression
Hypotheses isline.l ⊢ ≤ ˙ = ≤ K
isline.j ⊢ ∨ ˙ = join ⁡ K
isline.a ⊢ A = Atoms ⁡ K
isline.n ⊢ N = Lines ⁡ K
Assertion isline ⊢ K ∈ D → X ∈ N ↔ ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ X = p ∈ A | p ≤ ˙ q ∨ ˙ r

Proof

Step Hyp Ref Expression
1 isline.l ⊢ ≤ ˙ = ≤ K
2 isline.j ⊢ ∨ ˙ = join ⁡ K
3 isline.a ⊢ A = Atoms ⁡ K
4 isline.n ⊢ N = Lines ⁡ K
5 1 2 3 4 lineset ⊢ K ∈ D → N = x | ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ x = p ∈ A | p ≤ ˙ q ∨ ˙ r
6 5 eleq2d ⊢ K ∈ D → X ∈ N ↔ X ∈ x | ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ x = p ∈ A | p ≤ ˙ q ∨ ˙ r
7 3 fvexi ⊢ A ∈ V
8 7 rabex ⊢ p ∈ A | p ≤ ˙ q ∨ ˙ r ∈ V
9 eleq1 ⊢ X = p ∈ A | p ≤ ˙ q ∨ ˙ r → X ∈ V ↔ p ∈ A | p ≤ ˙ q ∨ ˙ r ∈ V
10 8 9 mpbiri ⊢ X = p ∈ A | p ≤ ˙ q ∨ ˙ r → X ∈ V
11 10 adantl ⊢ q ≠ r ∧ X = p ∈ A | p ≤ ˙ q ∨ ˙ r → X ∈ V
12 11 a1i ⊢ q ∈ A ∧ r ∈ A → q ≠ r ∧ X = p ∈ A | p ≤ ˙ q ∨ ˙ r → X ∈ V
13 12 rexlimivv ⊢ ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ X = p ∈ A | p ≤ ˙ q ∨ ˙ r → X ∈ V
14 eqeq1 ⊢ x = X → x = p ∈ A | p ≤ ˙ q ∨ ˙ r ↔ X = p ∈ A | p ≤ ˙ q ∨ ˙ r
15 14 anbi2d ⊢ x = X → q ≠ r ∧ x = p ∈ A | p ≤ ˙ q ∨ ˙ r ↔ q ≠ r ∧ X = p ∈ A | p ≤ ˙ q ∨ ˙ r
16 15 2rexbidv ⊢ x = X → ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ x = p ∈ A | p ≤ ˙ q ∨ ˙ r ↔ ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ X = p ∈ A | p ≤ ˙ q ∨ ˙ r
17 13 16 elab3 ⊢ X ∈ x | ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ x = p ∈ A | p ≤ ˙ q ∨ ˙ r ↔ ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ X = p ∈ A | p ≤ ˙ q ∨ ˙ r
18 6 17 bitrdi ⊢ K ∈ D → X ∈ N ↔ ∃ q ∈ A ∃ r ∈ A q ≠ r ∧ X = p ∈ A | p ≤ ˙ q ∨ ˙ r