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 )