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
|- A = ( Atoms ` K )
pexmidALT.p
|- .+ = ( +P ` K )
pexmidALT.o
|- ._|_ = ( _|_P ` K )
Assertion pexmidlem8N
|- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) = A )

Proof

Step Hyp Ref Expression
1 pexmidALT.a
 |-  A = ( Atoms ` K )
2 pexmidALT.p
 |-  .+ = ( +P ` K )
3 pexmidALT.o
 |-  ._|_ = ( _|_P ` K )
4 nonconne
 |-  -. ( X = X /\ X =/= X )
5 simpll
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> K e. HL )
6 simplr
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> X C_ A )
7 1 3 polssatN
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A )
8 7 adantr
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( ._|_ ` X ) C_ A )
9 1 2 paddssat
 |-  ( ( K e. HL /\ X C_ A /\ ( ._|_ ` X ) C_ A ) -> ( X .+ ( ._|_ ` X ) ) C_ A )
10 5 6 8 9 syl3anc
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) C_ A )
11 df-pss
 |-  ( ( X .+ ( ._|_ ` X ) ) C. A <-> ( ( X .+ ( ._|_ ` X ) ) C_ A /\ ( X .+ ( ._|_ ` X ) ) =/= A ) )
12 pssnel
 |-  ( ( X .+ ( ._|_ ` X ) ) C. A -> E. p ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) )
13 11 12 sylbir
 |-  ( ( ( X .+ ( ._|_ ` X ) ) C_ A /\ ( X .+ ( ._|_ ` X ) ) =/= A ) -> E. p ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) )
14 df-rex
 |-  ( E. p e. A -. p e. ( X .+ ( ._|_ ` X ) ) <-> E. p ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) )
15 13 14 sylibr
 |-  ( ( ( X .+ ( ._|_ ` X ) ) C_ A /\ ( X .+ ( ._|_ ` X ) ) =/= A ) -> E. p e. A -. p e. ( X .+ ( ._|_ ` X ) ) )
16 simplll
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> K e. HL )
17 simpllr
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X C_ A )
18 simprl
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> p e. A )
19 simplrl
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
20 simplrr
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> X =/= (/) )
21 simprr
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> -. p e. ( X .+ ( ._|_ ` X ) ) )
22 eqid
 |-  ( le ` K ) = ( le ` K )
23 eqid
 |-  ( join ` K ) = ( join ` K )
24 eqid
 |-  ( X .+ { p } ) = ( X .+ { p } )
25 22 23 1 2 3 24 pexmidlem6N
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X .+ { p } ) = X )
26 22 23 1 2 3 24 pexmidlem7N
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X .+ { p } ) =/= X )
27 25 26 jca
 |-  ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( X .+ { p } ) = X /\ ( X .+ { p } ) =/= X ) )
28 16 17 18 19 20 21 27 syl33anc
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( X .+ { p } ) = X /\ ( X .+ { p } ) =/= X ) )
29 nonconne
 |-  -. ( ( X .+ { p } ) = X /\ ( X .+ { p } ) =/= X )
30 29 4 2false
 |-  ( ( ( X .+ { p } ) = X /\ ( X .+ { p } ) =/= X ) <-> ( X = X /\ X =/= X ) )
31 28 30 sylib
 |-  ( ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) /\ ( p e. A /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( X = X /\ X =/= X ) )
32 31 rexlimdvaa
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( E. p e. A -. p e. ( X .+ ( ._|_ ` X ) ) -> ( X = X /\ X =/= X ) ) )
33 15 32 syl5
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( ( ( X .+ ( ._|_ ` X ) ) C_ A /\ ( X .+ ( ._|_ ` X ) ) =/= A ) -> ( X = X /\ X =/= X ) ) )
34 10 33 mpand
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( ( X .+ ( ._|_ ` X ) ) =/= A -> ( X = X /\ X =/= X ) ) )
35 34 necon1bd
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( -. ( X = X /\ X =/= X ) -> ( X .+ ( ._|_ ` X ) ) = A ) )
36 4 35 mpi
 |-  ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) = A )