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

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 ∧ 𝑋 ⊆ 𝐴 ) ∧ ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ∧ 𝑋 ≠ ∅ ) ) → ( 𝑋 + ( ⊥ ‘ 𝑋 ) ) = 𝐴 )