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

Metamath Proof Explorer

Theorem 1dimN

Description: An atom is covered by a height-2 element (1-dimensional line). (Contributed by NM, 3-May-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2dim.j ⊢ ∨ = ( join ‘ 𝐾 )
2dim.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
2dim.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 1dimN ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) )

Proof

Step Hyp Ref Expression
1 2dim.j ⊢ ∨ = ( join ‘ 𝐾 )
2 2dim.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3 2dim.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 2dim ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
5 r19.42v ⊢ ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ∃ 𝑟 ∈ 𝐴 ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
6 5 simplbi ⊢ ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) → 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) )
7 6 reximi ⊢ ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) → ∃ 𝑞 ∈ 𝐴 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) )
8 4 7 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) )