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

Metamath Proof Explorer

Theorem lhpex2leN

Description: There exist at least two different atoms under a co-atom. This allows to create a line under the co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lhp2at.l ⊢ ≤ ˙ = ≤ K
lhp2at.a ⊢ A = Atoms ⁡ K
lhp2at.h ⊢ H = LHyp ⁡ K
Assertion lhpex2leN ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A ∃ q ∈ A p ≤ ˙ W ∧ q ≤ ˙ W ∧ p ≠ q

Proof

Step Hyp Ref Expression
1 lhp2at.l ⊢ ≤ ˙ = ≤ K
2 lhp2at.a ⊢ A = Atoms ⁡ K
3 lhp2at.h ⊢ H = LHyp ⁡ K
4 simprr ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ A ∧ p ≤ ˙ W → p ≤ ˙ W
5 1 2 3 lhpexle1 ⊢ K ∈ HL ∧ W ∈ H → ∃ q ∈ A q ≤ ˙ W ∧ q ≠ p
6 5 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ A ∧ p ≤ ˙ W → ∃ q ∈ A q ≤ ˙ W ∧ q ≠ p
7 4 6 jca ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ A ∧ p ≤ ˙ W → p ≤ ˙ W ∧ ∃ q ∈ A q ≤ ˙ W ∧ q ≠ p
8 necom ⊢ p ≠ q ↔ q ≠ p
9 8 3anbi3i ⊢ p ≤ ˙ W ∧ q ≤ ˙ W ∧ p ≠ q ↔ p ≤ ˙ W ∧ q ≤ ˙ W ∧ q ≠ p
10 3anass ⊢ p ≤ ˙ W ∧ q ≤ ˙ W ∧ q ≠ p ↔ p ≤ ˙ W ∧ q ≤ ˙ W ∧ q ≠ p
11 9 10 bitri ⊢ p ≤ ˙ W ∧ q ≤ ˙ W ∧ p ≠ q ↔ p ≤ ˙ W ∧ q ≤ ˙ W ∧ q ≠ p
12 11 rexbii ⊢ ∃ q ∈ A p ≤ ˙ W ∧ q ≤ ˙ W ∧ p ≠ q ↔ ∃ q ∈ A p ≤ ˙ W ∧ q ≤ ˙ W ∧ q ≠ p
13 r19.42v ⊢ ∃ q ∈ A p ≤ ˙ W ∧ q ≤ ˙ W ∧ q ≠ p ↔ p ≤ ˙ W ∧ ∃ q ∈ A q ≤ ˙ W ∧ q ≠ p
14 12 13 bitr2i ⊢ p ≤ ˙ W ∧ ∃ q ∈ A q ≤ ˙ W ∧ q ≠ p ↔ ∃ q ∈ A p ≤ ˙ W ∧ q ≤ ˙ W ∧ p ≠ q
15 7 14 sylib ⊢ K ∈ HL ∧ W ∈ H ∧ p ∈ A ∧ p ≤ ˙ W → ∃ q ∈ A p ≤ ˙ W ∧ q ≤ ˙ W ∧ p ≠ q
16 1 2 3 lhpexle ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A p ≤ ˙ W
17 15 16 reximddv ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A ∃ q ∈ A p ≤ ˙ W ∧ q ≤ ˙ W ∧ p ≠ q