Metamath Proof Explorer


Theorem lhpexle3

Description: There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses lhpex1.l = ( le ‘ 𝐾 )
lhpex1.a 𝐴 = ( Atoms ‘ 𝐾 )
lhpex1.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexle3 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌𝑝𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l = ( le ‘ 𝐾 )
2 lhpex1.a 𝐴 = ( Atoms ‘ 𝐾 )
3 lhpex1.h 𝐻 = ( LHyp ‘ 𝐾 )
4 1 2 3 lhpexle2 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) )
5 3anass ( ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) ↔ ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ) )
6 5 rexbii ( ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑌 ) ↔ ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ) )
7 4 6 sylib ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ) )
8 1 2 3 lhpexle2 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑍 ) )
9 8 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑍 ) )
10 3anass ( ( 𝑝 𝑊𝑝𝑋𝑝𝑍 ) ↔ ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ) )
11 10 rexbii ( ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑋𝑝𝑍 ) ↔ ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ) )
12 9 11 sylib ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ) )
13 1 2 3 lhpexle2 ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑌𝑝𝑍 ) )
14 3anass ( ( 𝑝 𝑊𝑝𝑌𝑝𝑍 ) ↔ ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ) )
15 14 rexbii ( ∃ 𝑝𝐴 ( 𝑝 𝑊𝑝𝑌𝑝𝑍 ) ↔ ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ) )
16 13 15 sylib ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ) )
17 16 3ad2ant1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ) )
18 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
19 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → 𝑌𝐴 )
20 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → 𝑍𝐴 )
21 simprl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → 𝑋𝐴 )
22 simpl3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → 𝑌 𝑊 )
23 simpl2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → 𝑍 𝑊 )
24 simprr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → 𝑋 𝑊 )
25 1 2 3 lhpexle3lem ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑌𝐴𝑍𝐴𝑋𝐴 ) ∧ ( 𝑌 𝑊𝑍 𝑊𝑋 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍𝑝𝑋 ) ) )
26 18 19 20 21 22 23 24 25 syl133anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍𝑝𝑋 ) ) )
27 df-3an ( ( 𝑝𝑌𝑝𝑍𝑝𝑋 ) ↔ ( ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) )
28 27 anbi2i ( ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍𝑝𝑋 ) ) ↔ ( 𝑝 𝑊 ∧ ( ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) ) )
29 3anass ( ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) ↔ ( 𝑝 𝑊 ∧ ( ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) ) )
30 28 29 bitr4i ( ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍𝑝𝑋 ) ) ↔ ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) )
31 30 rexbii ( ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍𝑝𝑋 ) ) ↔ ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) )
32 26 31 sylib ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) ∧ ( 𝑋𝐴𝑋 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) )
33 17 32 lhpexle1lem ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) )
34 an31 ( ( ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) ↔ ( ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) )
35 34 anbi2i ( ( 𝑝 𝑊 ∧ ( ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) ) ↔ ( 𝑝 𝑊 ∧ ( ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) ) )
36 3anass ( ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) ↔ ( 𝑝 𝑊 ∧ ( ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) ) )
37 35 29 36 3bitr4i ( ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) ↔ ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) )
38 37 rexbii ( ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑌𝑝𝑍 ) ∧ 𝑝𝑋 ) ↔ ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) )
39 33 38 sylib ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) )
40 39 3expa ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ) ∧ ( 𝑌𝐴𝑌 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) )
41 12 40 lhpexle1lem ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) )
42 an32 ( ( ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) ↔ ( ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) )
43 42 anbi2i ( ( 𝑝 𝑊 ∧ ( ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) ) ↔ ( 𝑝 𝑊 ∧ ( ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) ) )
44 3anass ( ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) ↔ ( 𝑝 𝑊 ∧ ( ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) ) )
45 43 36 44 3bitr4i ( ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) ↔ ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) )
46 45 rexbii ( ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑍 ) ∧ 𝑝𝑌 ) ↔ ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) )
47 41 46 sylib ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑍𝐴𝑍 𝑊 ) ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) )
48 7 47 lhpexle1lem ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) )
49 df-3an ( ( 𝑝𝑋𝑝𝑌𝑝𝑍 ) ↔ ( ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) )
50 49 anbi2i ( ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌𝑝𝑍 ) ) ↔ ( 𝑝 𝑊 ∧ ( ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) ) )
51 44 50 bitr4i ( ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) ↔ ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌𝑝𝑍 ) ) )
52 51 rexbii ( ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌 ) ∧ 𝑝𝑍 ) ↔ ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌𝑝𝑍 ) ) )
53 48 52 sylib ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ( 𝑝 𝑊 ∧ ( 𝑝𝑋𝑝𝑌𝑝𝑍 ) ) )