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 ⊢ ≤ = ( le ‘ 𝐾 )
isline.j ⊢ ∨ = ( join ‘ 𝐾 )
isline.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
isline.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
Assertion isline ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )

Proof

Step Hyp Ref Expression
1 isline.l ⊢ ≤ = ( le ‘ 𝐾 )
2 isline.j ⊢ ∨ = ( join ‘ 𝐾 )
3 isline.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 isline.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
5 1 2 3 4 lineset ⊢ ( 𝐾 ∈ 𝐷 → 𝑁 = { 𝑥 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )
6 5 eleq2d ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑁 ↔ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ) )
7 3 fvexi ⊢ 𝐴 ∈ V
8 7 rabex ⊢ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ∈ V
9 eleq1 ⊢ ( 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } → ( 𝑋 ∈ V ↔ { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ∈ V ) )
10 8 9 mpbiri ⊢ ( 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } → 𝑋 ∈ V )
11 10 adantl ⊢ ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) → 𝑋 ∈ V )
12 11 a1i ⊢ ( ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) → 𝑋 ∈ V ) )
13 12 rexlimivv ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) → 𝑋 ∈ V )
14 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ↔ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
15 14 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ↔ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
16 15 2rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
17 13 16 elab3 ⊢ ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑥 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
18 6 17 bitrdi ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )