Theorem pexmidlem7N

Description: Lemma for pexmidN . Contradict pexmidlem6N . (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pexmidlem.l	⊢ ≤ = ( le ‘ 𝐾 )
	pexmidlem.j	⊢ ∨ = ( join ‘ 𝐾 )
	pexmidlem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pexmidlem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
	pexmidlem.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
	pexmidlem.m	⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
Assertion	pexmidlem7N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑀 ≠ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		pexmidlem.l	⊢ ≤ = ( le ‘ 𝐾 )
2		pexmidlem.j	⊢ ∨ = ( join ‘ 𝐾 )
3		pexmidlem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		pexmidlem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
5		pexmidlem.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
6		pexmidlem.m	⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
7		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝐾 ∈ HL )
8		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑝 ∈ 𝐴 )
9	8	snssd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → { 𝑝 } ⊆ 𝐴 )
10		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑋 ⊆ 𝐴 )
11	3 4	sspadd2	⊢ ( ( 𝐾 ∈ HL ∧ { 𝑝 } ⊆ 𝐴 ∧ 𝑋 ⊆ 𝐴 ) → { 𝑝 } ⊆ ( 𝑋 + { 𝑝 } ) )
12	7 9 10 11	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → { 𝑝 } ⊆ ( 𝑋 + { 𝑝 } ) )
13		vex	⊢ 𝑝 ∈ V
14	13	snss	⊢ ( 𝑝 ∈ ( 𝑋 + { 𝑝 } ) ↔ { 𝑝 } ⊆ ( 𝑋 + { 𝑝 } ) )
15	12 14	sylibr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑝 ∈ ( 𝑋 + { 𝑝 } ) )
16	15 6	eleqtrrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑝 ∈ 𝑀 )
17	3 5	polssatN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 )
18	7 10 17	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 )
19	3 4	sspadd1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) )
20	7 10 18 19	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑋 ⊆ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) )
21		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) )
22	20 21	ssneldd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → ¬ 𝑝 ∈ 𝑋 )
23		nelne1	⊢ ( ( 𝑝 ∈ 𝑀 ∧ ¬ 𝑝 ∈ 𝑋 ) → 𝑀 ≠ 𝑋 )
24	16 22 23	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) ) ) → 𝑀 ≠ 𝑋 )