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	⊢ ≤ = ( le ‘ 𝐾 )
		lhp2at.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
		lhp2at.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	Assertion	lhpex2leN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) )

Proof

Step	Hyp	Ref	Expression
1		lhp2at.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lhp2at.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		lhp2at.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		simprr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑊 ) ) → 𝑝 ≤ 𝑊 )
5	1 2 3	lhpexle1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) )
6	5	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) )
7	4 6	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑊 ) ) → ( 𝑝 ≤ 𝑊 ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) ) )
8		necom	⊢ ( 𝑝 ≠ 𝑞 ↔ 𝑞 ≠ 𝑝 )
9	8	3anbi3i	⊢ ( ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) ↔ ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) )
10		3anass	⊢ ( ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) ) )
11	9 10	bitri	⊢ ( ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) ↔ ( 𝑝 ≤ 𝑊 ∧ ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) ) )
12	11	rexbii	⊢ ( ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) ) )
13		r19.42v	⊢ ( ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) ) ↔ ( 𝑝 ≤ 𝑊 ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) ) )
14	12 13	bitr2i	⊢ ( ( 𝑝 ≤ 𝑊 ∧ ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≤ 𝑊 ∧ 𝑞 ≠ 𝑝 ) ) ↔ ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) )
15	7 14	sylib	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) )
16	1 2 3	lhpexle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑊 )
17	15 16	reximddv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) )