Metamath Proof Explorer

Theorem chirredlem4

Description: Lemma for chirredi . (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses chirred.1 
|- A e. CH
chirred.2 
|- ( x e. CH -> A C_H x )
Assertion chirredlem4 
|- ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r = p \/ r = q ) )

Proof

Step Hyp Ref Expression
1 chirred.1 
 |-  A e. CH
2 chirred.2 
 |-  ( x e. CH -> A C_H x )
3 atelch 
 |-  ( r e. HAtoms -> r e. CH )
4 breq2 
 |-  ( x = r -> ( A C_H x <-> A C_H r ) )
5 4 2 vtoclga 
 |-  ( r e. CH -> A C_H r )
6 3 5 syl 
 |-  ( r e. HAtoms -> A C_H r )
7 1 atordi 
 |-  ( ( r e. HAtoms /\ A C_H r ) -> ( r C_ A \/ r C_ ( _|_ ` A ) ) )
8 6 7 mpdan 
 |-  ( r e. HAtoms -> ( r C_ A \/ r C_ ( _|_ ` A ) ) )
9 8 ad2antrl 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r C_ A \/ r C_ ( _|_ ` A ) ) )
10 1 2 chirredlem3 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r C_ A -> r = p ) )
11 1 ococi 
 |-  ( _|_ ` ( _|_ ` A ) ) = A
12 11 sseq2i 
 |-  ( p C_ ( _|_ ` ( _|_ ` A ) ) <-> p C_ A )
13 12 biimpri 
 |-  ( p C_ A -> p C_ ( _|_ ` ( _|_ ` A ) ) )
14 atelch 
 |-  ( q e. HAtoms -> q e. CH )
15 atelch 
 |-  ( p e. HAtoms -> p e. CH )
16 chjcom 
 |-  ( ( q e. CH /\ p e. CH ) -> ( q vH p ) = ( p vH q ) )
17 14 15 16 syl2an 
 |-  ( ( q e. HAtoms /\ p e. HAtoms ) -> ( q vH p ) = ( p vH q ) )
18 17 sseq2d 
 |-  ( ( q e. HAtoms /\ p e. HAtoms ) -> ( r C_ ( q vH p ) <-> r C_ ( p vH q ) ) )
19 18 anbi2d 
 |-  ( ( q e. HAtoms /\ p e. HAtoms ) -> ( ( r e. HAtoms /\ r C_ ( q vH p ) ) <-> ( r e. HAtoms /\ r C_ ( p vH q ) ) ) )
20 19 ad2ant2r 
 |-  ( ( ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) /\ ( p e. HAtoms /\ p C_ ( _|_ ` ( _|_ ` A ) ) ) ) -> ( ( r e. HAtoms /\ r C_ ( q vH p ) ) <-> ( r e. HAtoms /\ r C_ ( p vH q ) ) ) )
21 1 choccli 
 |-  ( _|_ ` A ) e. CH
22 cmcm3 
 |-  ( ( A e. CH /\ x e. CH ) -> ( A C_H x <-> ( _|_ ` A ) C_H x ) )
23 1 22 mpan 
 |-  ( x e. CH -> ( A C_H x <-> ( _|_ ` A ) C_H x ) )
24 2 23 mpbid 
 |-  ( x e. CH -> ( _|_ ` A ) C_H x )
25 21 24 chirredlem3 
 |-  ( ( ( ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) /\ ( p e. HAtoms /\ p C_ ( _|_ ` ( _|_ ` A ) ) ) ) /\ ( r e. HAtoms /\ r C_ ( q vH p ) ) ) -> ( r C_ ( _|_ ` A ) -> r = q ) )
26 25 ex 
 |-  ( ( ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) /\ ( p e. HAtoms /\ p C_ ( _|_ ` ( _|_ ` A ) ) ) ) -> ( ( r e. HAtoms /\ r C_ ( q vH p ) ) -> ( r C_ ( _|_ ` A ) -> r = q ) ) )
27 20 26 sylbird 
 |-  ( ( ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) /\ ( p e. HAtoms /\ p C_ ( _|_ ` ( _|_ ` A ) ) ) ) -> ( ( r e. HAtoms /\ r C_ ( p vH q ) ) -> ( r C_ ( _|_ ` A ) -> r = q ) ) )
28 13 27 sylanr2 
 |-  ( ( ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) /\ ( p e. HAtoms /\ p C_ A ) ) -> ( ( r e. HAtoms /\ r C_ ( p vH q ) ) -> ( r C_ ( _|_ ` A ) -> r = q ) ) )
29 28 imp 
 |-  ( ( ( ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) /\ ( p e. HAtoms /\ p C_ A ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r C_ ( _|_ ` A ) -> r = q ) )
30 29 ancom1s 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r C_ ( _|_ ` A ) -> r = q ) )
31 10 30 orim12d 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( ( r C_ A \/ r C_ ( _|_ ` A ) ) -> ( r = p \/ r = q ) ) )
32 9 31 mpd 
 |-  ( ( ( ( p e. HAtoms /\ p C_ A ) /\ ( q e. HAtoms /\ q C_ ( _|_ ` A ) ) ) /\ ( r e. HAtoms /\ r C_ ( p vH q ) ) ) -> ( r = p \/ r = q ) )