Theorem lhpexle1

Description: There exists an atom under a co-atom different from any given element. (Contributed by NM, 24-Jul-2013)

	Ref	Expression
Hypotheses	lhpex1.l	⊢ ≤ = ( le ‘ 𝐾 )
	lhpex1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lhpex1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion	lhpexle1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		lhpex1.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lhpex1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		lhpex1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4	1 2 3	lhpexle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑊 )
5		tru	⊢ ⊤
6	5	jctr	⊢ ( 𝑝 ≤ 𝑊 → ( 𝑝 ≤ 𝑊 ∧ ⊤ ) )
7	6	reximi	⊢ ( ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑊 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ) )
8	4 7	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ) )
9		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
10		simprl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐴 )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 3	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
13	12	ad2antlr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
14		eqid	⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
15	1 14 2 3	lhplt	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑋 ( lt ‘ 𝐾 ) 𝑊 )
16	11 14 2	2atlt	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑊 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) )
17	9 10 13 15 16	syl31anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) )
18		simp3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑝 ( lt ‘ 𝐾 ) 𝑊 )
19		simp1ll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝐾 ∈ HL )
20		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑝 ∈ 𝐴 )
21		simp1lr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑊 ∈ 𝐻 )
22	1 14	pltle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑝 ( lt ‘ 𝐾 ) 𝑊 → 𝑝 ≤ 𝑊 ) )
23	19 20 21 22	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → ( 𝑝 ( lt ‘ 𝐾 ) 𝑊 → 𝑝 ≤ 𝑊 ) )
24	18 23	mpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑝 ≤ 𝑊 )
25		trud	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → ⊤ )
26		simp3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → 𝑝 ≠ 𝑋 )
27	24 25 26	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) ) → ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) )
28	27	3expia	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) → ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) ) )
29	28	reximdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≠ 𝑋 ∧ 𝑝 ( lt ‘ 𝐾 ) 𝑊 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) ) )
30	17 29	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) )
31	8 30	lhpexle1lem	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) )
32		3simpb	⊢ ( ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) → ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )
33	32	reximi	⊢ ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ ⊤ ∧ 𝑝 ≠ 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )
34	31 33	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ) )