Metamath Proof Explorer


Theorem pexmidlem8N

Description: Lemma for pexmidN . The contradiction of pexmidlem6N and pexmidlem7N shows that there can be no atom p that is not in X .+ ( ._|_X ) , which is therefore the whole atom space. (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pexmidALT.a 𝐴 = ( Atoms ‘ 𝐾 )
pexmidALT.p + = ( +𝑃𝐾 )
pexmidALT.o = ( ⊥𝑃𝐾 )
Assertion pexmidlem8N ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → ( 𝑋 + ( 𝑋 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 pexmidALT.a 𝐴 = ( Atoms ‘ 𝐾 )
2 pexmidALT.p + = ( +𝑃𝐾 )
3 pexmidALT.o = ( ⊥𝑃𝐾 )
4 nonconne ¬ ( 𝑋 = 𝑋𝑋𝑋 )
5 simpll ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → 𝐾 ∈ HL )
6 simplr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → 𝑋𝐴 )
7 1 3 polssatN ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) → ( 𝑋 ) ⊆ 𝐴 )
8 7 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → ( 𝑋 ) ⊆ 𝐴 )
9 1 2 paddssat ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ∧ ( 𝑋 ) ⊆ 𝐴 ) → ( 𝑋 + ( 𝑋 ) ) ⊆ 𝐴 )
10 5 6 8 9 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → ( 𝑋 + ( 𝑋 ) ) ⊆ 𝐴 )
11 df-pss ( ( 𝑋 + ( 𝑋 ) ) ⊊ 𝐴 ↔ ( ( 𝑋 + ( 𝑋 ) ) ⊆ 𝐴 ∧ ( 𝑋 + ( 𝑋 ) ) ≠ 𝐴 ) )
12 pssnel ( ( 𝑋 + ( 𝑋 ) ) ⊊ 𝐴 → ∃ 𝑝 ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) )
13 11 12 sylbir ( ( ( 𝑋 + ( 𝑋 ) ) ⊆ 𝐴 ∧ ( 𝑋 + ( 𝑋 ) ) ≠ 𝐴 ) → ∃ 𝑝 ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) )
14 df-rex ( ∃ 𝑝𝐴 ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ↔ ∃ 𝑝 ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) )
15 13 14 sylibr ( ( ( 𝑋 + ( 𝑋 ) ) ⊆ 𝐴 ∧ ( 𝑋 + ( 𝑋 ) ) ≠ 𝐴 ) → ∃ 𝑝𝐴 ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) )
16 simplll ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → 𝐾 ∈ HL )
17 simpllr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → 𝑋𝐴 )
18 simprl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → 𝑝𝐴 )
19 simplrl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → ( ‘ ( 𝑋 ) ) = 𝑋 )
20 simplrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → 𝑋 ≠ ∅ )
21 simprr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) )
22 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
23 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
24 eqid ( 𝑋 + { 𝑝 } ) = ( 𝑋 + { 𝑝 } )
25 22 23 1 2 3 24 pexmidlem6N ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴𝑝𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → ( 𝑋 + { 𝑝 } ) = 𝑋 )
26 22 23 1 2 3 24 pexmidlem7N ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴𝑝𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → ( 𝑋 + { 𝑝 } ) ≠ 𝑋 )
27 25 26 jca ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴𝑝𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → ( ( 𝑋 + { 𝑝 } ) = 𝑋 ∧ ( 𝑋 + { 𝑝 } ) ≠ 𝑋 ) )
28 16 17 18 19 20 21 27 syl33anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → ( ( 𝑋 + { 𝑝 } ) = 𝑋 ∧ ( 𝑋 + { 𝑝 } ) ≠ 𝑋 ) )
29 nonconne ¬ ( ( 𝑋 + { 𝑝 } ) = 𝑋 ∧ ( 𝑋 + { 𝑝 } ) ≠ 𝑋 )
30 29 4 2false ( ( ( 𝑋 + { 𝑝 } ) = 𝑋 ∧ ( 𝑋 + { 𝑝 } ) ≠ 𝑋 ) ↔ ( 𝑋 = 𝑋𝑋𝑋 ) )
31 28 30 sylib ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) ∧ ( 𝑝𝐴 ∧ ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) ) ) → ( 𝑋 = 𝑋𝑋𝑋 ) )
32 31 rexlimdvaa ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → ( ∃ 𝑝𝐴 ¬ 𝑝 ∈ ( 𝑋 + ( 𝑋 ) ) → ( 𝑋 = 𝑋𝑋𝑋 ) ) )
33 15 32 syl5 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → ( ( ( 𝑋 + ( 𝑋 ) ) ⊆ 𝐴 ∧ ( 𝑋 + ( 𝑋 ) ) ≠ 𝐴 ) → ( 𝑋 = 𝑋𝑋𝑋 ) ) )
34 10 33 mpand ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → ( ( 𝑋 + ( 𝑋 ) ) ≠ 𝐴 → ( 𝑋 = 𝑋𝑋𝑋 ) ) )
35 34 necon1bd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → ( ¬ ( 𝑋 = 𝑋𝑋𝑋 ) → ( 𝑋 + ( 𝑋 ) ) = 𝐴 ) )
36 4 35 mpi ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐴 ) ∧ ( ( ‘ ( 𝑋 ) ) = 𝑋𝑋 ≠ ∅ ) ) → ( 𝑋 + ( 𝑋 ) ) = 𝐴 )